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.

Estimated changes