Commit 2024-10-30 02:32 801cc3e5
View on Github →chore(scripts/mk_all): gracefully run loadWorkspace
(#17953)
Changes scripts/mk_all
to run loadWorkspace
using Lake's toBaseIO
utility. In addition to being a bit cleaner, this adaption will also be necessary once leanprover/lean4#5684 lands.