bors should not try to merge a PR if the CI has failed

[varkor]

trafficstars

In the rare occasions we might want to merge even if CI has failed, we should explicitly command @bors to ignore the CI failure.

[Mark-Simulacrum]

Why would this ever be the case? I'm quite confused -- is there some context here? Bors does check the CI status (otherwise, you know, there'd be no point...?)

[varkor]

Sorry, I thought someone indicated otherwise, and I must have misunderstood.

[Mark-Simulacrum]

Discussed briefly on Discord. Turns out @varkor presumably meant that if the PR CI fails, we should not then go and try to test on auto branch CI, since that's probably a waste of time.

[RalfJung]

Yeah, it would be great if bors either waited until PR CI passed before adding the PR to the queue, or else de-queued PRs (auto-bors r-) when PR CI fails.

[jyn514]

Maybe easier to implement - if bors could show on the queue that PR CI failed, it would at least let people know it wouldn't be included in rollups: https://github.com/rust-lang/rust/pull/84716#issuecomment-829706626

[jackh726]

Or better: if CI fails, then it automatically gets r-ed

Oh that was said

[camelid]

Another approach to this is r+ await (#120).