fix: prefer local search path

This commit is contained in:
Sebastian Ullrich 2021-10-22 12:48:37 +02:00
parent 91f1948f50
commit f202c7c322

View file

@ -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 := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }