mathlib
60c77d49 - feat(tactic/lint): include linter name in github output (#11413)

Commit

4 years ago

feat(tactic/lint): include linter name in github output (#11413) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author

robertylewis

Parents