mathlib
2c9d9bd0 - chore(scripts/nolints_summary.sh): list number of nolints per file

Commit

6 years ago

chore(scripts/nolints_summary.sh): list number of nolints per file

Author

jcommelin

jcommelin

Parents

Loading