mathlib
7a8f53e1
- feat(tactic/lint): silent linting (#1580)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
feat(tactic/lint): silent linting (#1580) * feat(tactic/lint): silent linting * doc(tactic/lint): doc silent linting and nolint features * fix test * change notation for silent linting * style(tactic/lint): remove commented lines
References
#1580 - feat(tactic/lint): silent linting
Author
robertylewis
Committer
mergify[bot]
Parents
94e368c5
Loading