The scenario was as follows:
3 PRs were scheduled for merging. When their batch started, one of them had their
r+ revoked by saying
r-. The 2 remaining PRs are
Canceled (will resume). Is there a way to merge those two independently / in a batch of 2?
It all started here: https://github.com/rchain/rchain/pull/2100#issuecomment-460205793
r+-ing the ohter 2 PRs, but got
Already running a review.
Would you agree that it’d make sense for bors to re-start a batch for the non-revoked PRs immediately, without waiting for the revoked one (especially that build results won’t be reused and it’ll take time till the revoked PR is fixed)?