From 971e6f5e3d2205a035d19e7a10a8a113976e4d35 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 19 Oct 2024 15:16:41 -0400 Subject: [PATCH] fix `scripts/mk_all` --- scripts/mk_all.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_all.lean b/scripts/mk_all.lean index f58f7491c65e6..ff77e78553883 100644 --- 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