Hi,
After this announcement from Github, bors is unable to merge PRs in batches and merges fail with this message:
This PR was included in a batch that successfully built, but then failed to merge into master. It will not be retried.
Additional information:
{"message":"Changes must be made through a pull request.","documentation_url":"https://docs.github.com/articles/about-protected-branches"}
We have added now added the bors-ng bot to the list of actors that can bypass required pull requests, and now batching works again, but this wasn't the case earlier.
What has changed?
Also batched PRs now gets closed after merging, and github seemingly randomly assigns "merged" or "closed" on the PRs after merge which is annoying in case your PR was merged successfully but github doesn't reflect the status correctly.
In short, you need to turn off the setting that requires reviews on pull requests. Instead, make "bors" a required-to-merge status, and configure the review requirements in bors.toml. This is how you should have always done it, because it won't work correctly with batches that contain more than one PR otherwise.
Alternatively, migrate to GitHub's built-in merge queue, which integrates correctly with this feature.
Hi @notriddle !
Thanks for the reply!
We have it set up with bors being able to bypass the pull request requirement now.
Have you noticed something with the statuses of PRs that were batch merged having different statuses (closed or merged) after successful merges?
Also strange that the PRs get closed automatically now after merge, it used to not be like that earlier and we haven't fiddled with that setting in our repo for a long time.