mathlib

c8c6d2e7 - feat(ci): Emit error messages in a way understood by github (#5726)

feat(ci): Emit error messages in a way understood by github (#5726) This uses the commands described [here](https://github.com/actions/toolkit/blob/master/docs/commands.md#log-level), for which [the implementation](https://github.com/actions/toolkit/blob/af821474235d3c5e1f49cee7c6cf636abb0874c4/packages/core/src/command.ts#L36-L94) provides a slightly clearer spec. This means github now annotates broken lines, and highlights the error in red. Originally I tried to implement this using "problem matchers", but these do not support multi-line error messages. Supporting this in the linter is something that I'll leave for a follow-up PR. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>