CI "check for noisy stdout lines"

Stream: mathlib4

[Jon Eugster]

I found the CI message here not very helpful:
CI-error.png

It took me a moment to figure out that this was because of a linter warning:

linter-warning.png

Could we improve this? I wonder if simply adding -A1 to the grep search would already do something?

[Alex J. Best]

Adding A1 would probably help quite a bit yes! If you make a PR I will review it. Its a bit tricky to do better because I don't think we get line numbers or anything for stdout lines so I dont think the CI can pin the message anywhere more sensible, even finding which file it comes from is annoying when the build is parallel

[Jon Eugster]

#7868