From f202c7c32218ea7b47bc94ae2983b2b36c047c79 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Oct 2021 12:48:37 +0200 Subject: [PATCH] fix: prefer local search path --- src/Lean/Server/FileWorker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 }