mathlib
945845d8 - feat(linter): include linter name in report (#2116)

Commit
6 years ago
feat(linter): include linter name in report (#2116) * feat(linter): include linter name in report (closes #2098) * Update src/tactic/lint.lean Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading