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;