mathlib
03344754 - ci(scripts/detect_errors): try to show info messages in a way github understands (#6493)

Commit
4 years ago
ci(scripts/detect_errors): try to show info messages in a way github understands (#6493) I don't actually know if this works, but I know that the previous code was not working: https://github.com/leanprover-community/mathlib/pull/6485/checks?check_run_id=2006396264#step:7:7 Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading