mathlib
78dc23ff
- chore(scripts/*): rename files of the style linter (#5605)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(scripts/*): rename files of the style linter (#5605) The style linter has been doing a bit more than just checking for copyright headers, module docstrings, or line lengths. So I thought it made sense to reflect that in the filenames.
Author
jcommelin
Parents
6dcfa5c2
Loading