adopt bors

[nikomatsakis]

We should adopt https://bors.tech/!

[youknowone]

The recent github merge queue also looks like shares similar features about queue
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue

[nikomatsakis]

Ah, nice, even better.

[nikomatsakis]

If somebody could check that our CI is compliant here, or prepare a PR otherwise, I can enable merge queues: 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 (I can't do this until later)

…

On Sat, Mar 25, 2023, at 12:22 PM, Jeong, YunWon wrote: The recent github merge queue also looks like shares similar features about queue https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue — Reply to this email directly, view it on GitHub <#720 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABF4ZVYIGWQQOT7DKLEOLLW54LUDANCNFSM6AAAAAAWHPPT44>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[youknowone]

I tested it with #733 and it works great. You will see Merge when ready button on PRs now.
This is cool feature. I'd better to set it up for other my repositories too.

[yannham]

@nikomatsakis I think merge queues are now enabled. I'm personally satisfied with it; do you think we should keep this issue open or we can close? Using GitHub's integrated solution has some obvious advantages.