Build failed: CI Success

Stream: mathlib4

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/pull/29914#issuecomment-3371259296

image.png

This apparently paradoxical message is caused by bors linking to the "CI Success" tab here:

image.png

I'm wondering if we can instead link to the failed tab and say "logs" in the text?

[Bryan Gin-ge Chen]

So the list of jobs shown in that message is controlled by bors.toml, and we used to list the "Build" and "Lint style" jobs as separate requirements there. This was changed in #25614 because I thought that it was necessary for PRs from forks to be able to merge. However, on thinking about this some more, I think I was wrong about that and we could try reverting the changes to bors.toml again so that the required jobs are all listed individually.

I'll try and put a PR together later today.

[Kenny Lau]

Thanks!

[Anne Baanen]

(If this PR doesn't work out, I propose we at least rename this job to "Check for CI success" or similar.)

[Bryan Gin-ge Chen]

I've opened #30283 for this.