Commit 2026-10-20 16:41 499b0ec1

View on Github →

chore: revert "feat: enable Verso if no syntax or doc-gen changes (#45031)" (#45094) This PR reverts commit bbe3db288201b39ef92689278906d3bf6d45c291. It turns out we triggered a Lean bug which causes the build to fail unexpectedly some of the time. I'd like to get this reverted first so things build, and then figure out what to do (wait for new release candidate, only enable Verso in a safe subset of files, ...) Zulip discussion starting here: #rss > Significant commits to mathlib4 @ 💬

Estimated changes