From bdd5185a7f80acc2ccf72ca238e608f5487c6a3b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Mar 2022 10:31:18 +0100 Subject: [PATCH] fix: `serve` + `print-paths` without lakefile --- Lake/CLI/Main.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 219d707c25..83bbea25ad 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -208,10 +208,10 @@ The `print-paths` command is used internally by Lean 4 server. def printPaths (imports : List String := []) : CliStateM PUnit := do let (lean, lake) ← getInstall let configFile := (← getRootDir) / (← getConfigFile) - if (← IO.getEnv invalidConfigEnvVar) matches some .. then - IO.eprintln s!"Error parsing '{configFile}'. Please restart the lean server after fixing the Lake configuration file." - exit 1 - else if (← configFile.pathExists) then + if (← configFile.pathExists) then + if (← IO.getEnv invalidConfigEnvVar) matches some .. then + IO.eprintln s!"Error parsing '{configFile}'. Please restart the lean server after fixing the Lake configuration file." + exit 1 let ws ← loadWorkspace (← getSubArgs) let ctx ← mkBuildContext ws lean lake ws.root.buildImportsAndDeps imports |>.run LogMethods.eio ctx