Stream: Coq devs & plugin devs

Topic: GitHub adds auto-merge

Emilio Jesús Gallego Arias (Jan 13 2021 at 09:28):

I see that github added auto-merge support recently, it may be of interest to some:
https://docs.github.com/en/free-pro-team@latest/github/collaborating-with-issues-and-pull-requests/automatically-merging-a-pull-request

Last updated: Apr 20 2024 at 08:02 UTC