PR #2116 feat(linter): include linter name in report

feat(linter): include linter name in report #2116

mergify merged 3 commits into master from nolint-names

feat(linter): include linter name in report (closes #2098)

8c71ec8b

kim-em commented on 2020-03-09

Update src/tactic/lint.lean

230fe0ae

kim-em approved these changes on 2020-03-09

kim-em added ready-to-merge

Merge branch 'master' into nolint-names

6cbebaf4

mergify merged 945845d8 into master 6 years ago

mergify deleted the nolint-names branch 6 years ago

Reviewers

kim-em

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone