max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: add Lake to built-in search path

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-19 10:56:38 +02:00
parent 6a90b30875
commit b3c8ee2923
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Server/FileWorker.lean
View file

@ -170,7 +170,8 @@ section Initialization
| some path => pure <| System.FilePath.mk path / "bin" / lakePath
| _ => pure <| (← appDir) / lakePath
lakePath.withExtension System.FilePath.exeExtension
let mut srcSearchPath := [(← appDir) / ".." / "lib" / "lean" / "src"]
let srcPath := (← appDir) / ".." / "lib" / "lean" / "src"
let mut srcSearchPath := [srcPath, srcPath / "lake"]
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
let (headerEnv, msgLog) ← try