chore: improve error

leanprover · Oct 13, 2023 · d0ae87d · d0ae87d
1 parent b534878
commit d0ae87d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
@@ -190,7 +190,7 @@ section Initialization
       paths.srcPath.mapM realPathNormalized
     | 2 => pure []  -- no lakefile.lean
     -- error from `--no-build`
-    | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Refresh File Dependencies\" command in your editor\n\n{stdout}"
+    | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor.\n\n{stdout}"
     | _ => throwServerError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}"
 
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)