From ba7d14ebc265ca024fe1ab3f34b132dcb8e5cb13 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2019 07:58:05 -0800 Subject: [PATCH] fix: default path --- src/Init/Lean/Path.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Path.lean b/src/Init/Lean/Path.lean index dee7bbce67..804404dc1c 100644 --- a/src/Init/Lean/Path.lean +++ b/src/Init/Lean/Path.lean @@ -45,7 +45,7 @@ def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath := def getBuiltinSearchPath : IO SearchPath := do appDir ← IO.appDir; - let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "library" ++ pathSep ++ "Init"; + let libDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "src" ++ pathSep ++ "Init"; libDirExists ← IO.isDir libDir; if libDirExists then do path ← realPathNormalized libDir;