New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Migrate away from bors, use a Github merge queue instead. #742

Closed

jswrenn opened this issue Aug 31, 2023 · 0 comments · Fixed by #773

Labels

Member

jswrenn commented Aug 31, 2023

Bors is deprecated and the public instance will be shutting down. We should migrate to a Github merge queue instead.

jswrenn added the help wanted label

jswrenn added a commit that referenced this issue


          Configure CI for merge_queue.

53d0631

Fixes #742.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions

jswrenn mentioned this issue

Configure CI for merge_queue. #773

Merged

jswrenn added a commit that referenced this issue


          Configure CI for merge_queue.

d78794e

Fixes #742.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions

jswrenn added a commit that referenced this issue


          Configure CI for merge_queue.

cb090b7

Fixes #742.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions

jswrenn added a commit that referenced this issue


          Configure CI for merge_queue.

9b94950

Fixes #742.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions

github-merge-queue bot pushed a commit that referenced this issue


          Configure CI for merge_queue.

c4358ab

Fixes #742.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions

jswrenn closed this as completed in #773

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment