Stream: Coq devs & plugin devs

Topic: GitHub adds auto-merge


view this post on Zulip 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: Oct 21 2021 at 21:03 UTC