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

refacttor: check LEAN_SYSROOT rather than LEAN_HOME for Lean

Browse source
This commit is contained in:
tydeu 2021-10-07 14:04:18 -04:00
parent 9700208501
commit 1d20cbd3d6
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/InstallPath.lean
View file

@ -61,7 +61,7 @@ def findLakeLeanJointHome? : IO (Option FilePath) := do
/--
Try to find Lean's installation path by
first checking the `LEAN_HOME` environment variable
first checking the `LEAN_SYSROOT` environment variable
and then by trying `findLeanPathHome?`.
It assumes that the Lean installation is setup the normal way.
@ -69,7 +69,7 @@ def findLakeLeanJointHome? : IO (Option FilePath) := do
libraries and `.olean` files located in `<lean-home>/lib/lean`.
-/
def findLeanInstall? : IO (Option LeanInstall) := do
if let some home ← IO.getEnv "LEAN_HOME" then
if let some home ← IO.getEnv "LEAN_SYSROOT" then
return some {home}
if let some home ← findLeanPathHome? then
return some {home}