Skip to content

Conversation

@jdtournier
Copy link
Member

The plan is to make use of GitHub's new merge queue feature, to reduce the faff when trying to merge multiple pull requests at the same time. More detail on the GitHub docs:
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue

Note that this has been activated on master.

The plan is to make use of GitHub's new merge queue feature, to reduce
the faff when trying to merge multiple pull requests at the same time.
More detail on the GitHub docs:
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue

Note that this has been activated on master.
@jdtournier jdtournier requested a review from a team February 17, 2023 11:20
@jdtournier jdtournier self-assigned this Feb 17, 2023
@jdtournier jdtournier enabled auto-merge February 17, 2023 11:21
@jdtournier jdtournier added this pull request to the merge queue Feb 17, 2023
Merged via the queue into master with commit 3166003 Feb 17, 2023
@jdtournier jdtournier deleted the update_CI_for_github_merge_queue branch February 17, 2023 19:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants