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
I’ve tried 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)?
Cheers!