Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-02-04 03:54
c4bcf3ac
View on Github →
chore(scripts): update nolints.txt (
#18385
) I am happy to remove some nolints for you!
Estimated changes
Modified
scripts/nolints.txt
Modified
scripts/style-exceptions.txt