feat(tactic/lint): include linter name in github output (#11413)
feat(tactic/lint): include linter name in github output (#11413)




Co-authored-by: Rob Lewis <597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib