Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-10-18 00:25
9d68c2ad
View on Github →
chore(scripts): update nolints.json (
#44984
) I am happy to remove some nolints for you!
Estimated changes
Modified
scripts/nolints.json