Mathlib Changelog
Changelog
About
Github
Commit
2023-05-23 04:16
cb9077f7
View on Github →
chore(scripts): update nolints.txt (
#19065
) I am happy to remove some nolints for you!
Estimated changes
Modified
scripts/nolints.txt
Modified
scripts/style-exceptions.txt