Commit 2022-01-11 13:55 be4c5aa4
View on Github →feat(scripts/lint_mathlib): implement github annotations for mathlib linters (#11345)
Resolves the last part of #5863
This causes lean --run lint_mathlib --github to produce error messages understood by github actions, which will tag the lines causing linter failures with annotations in the files changed tab