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

fix: default LEAN_PATH for installed Lean

Browse source
This commit is contained in:
Sebastian Ullrich 2020-01-25 15:58:06 +01:00
parent 5c0fa84af5
commit 88fe0de284
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/Init/Lean/Util/Path.lean
View file

@ -51,7 +51,7 @@ if libDirExists then do
path ← realPathNormalized libDir;
pure $ HashMap.empty.insert "Init" path
else do
let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "library" ++ pathSep ++ "Init";
let installedLibDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Init";
installedLibDirExists ← IO.isDir installedLibDir;
if installedLibDirExists then do
path ← realPathNormalized installedLibDir;