From 88fe0de2849f5e0788a5e1992cd7ac2b33b8589e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 25 Jan 2020 15:58:06 +0100
Subject: [PATCH] fix: default LEAN_PATH for installed Lean

---
 src/Init/Lean/Util/Path.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean
index 2bfeb1e776..964bbafe9b 100644
--- a/src/Init/Lean/Util/Path.lean
+++ b/src/Init/Lean/Util/Path.lean
@@ -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;