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

fix: prefer user-given search paths

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

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

@ -172,7 +172,7 @@ section Initialization
lakePath.withExtension System.FilePath.exeExtension
let mut srcSearchPath := [(← appDir) / ".." / "lib" / "lean" / "src"]
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := srcSearchPath ++ System.SearchPath.parse p
srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
let (headerEnv, msgLog) ← try
-- NOTE: lake does not exist in stage 0 (yet?)
if (← System.FilePath.pathExists lakePath) then