We also add "." (i.e., current directory) if `LEAN_PATH` is not defined. Users may still override stdlib since we add the builtin search path in the end. @dselsam You should now be able to compile your project without setting `LEAN_PATH` cc @kha |
||
|---|---|---|
| .. | ||
| init | ||
| library.md | ||
| Makefile.in | ||
| relative.py | ||