diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 48706c6134..b8b729c544 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -179,7 +179,7 @@ section Initialization -- NOTE: lake does not exist in stage 0 (yet?) if (← System.FilePath.pathExists lakePath) then let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut - srcSearchPath := srcSearchPath ++ pkgSearchPath + srcSearchPath := pkgSearchPath ++ srcSearchPath Elab.processHeader headerStx opts msgLog inputCtx catch e => -- should be from `lake print-paths` let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString }