fix scripts/mk_all

leanprover-community · Oct 19, 2024 · 971e6f5 · 971e6f5
1 parent 33e27ef
commit 971e6f5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/scripts/mk_all.lean b/scripts/mk_all.lean
@@ -26,7 +26,8 @@ it includes `Mathlib/Tactic`. -/
 def getLeanLibs : IO (Array String) := do
   let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
   let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
-  let ws ← MonadError.runEIO (MainM.runLogIO (loadWorkspace config)).toEIO
+  let some ws ← loadWorkspace config |>.toBaseIO
+    | throw <| IO.userError "failed to load Lake workspace"
   let package := ws.root
   let libs := (package.leanLibs.map (·.name)).map (·.toString)
   return if package.name == `mathlib then