Emilio Jesús Gallego Arias (Jan 13 2021 at 09:28): 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 08 2024 at 14:01 UTC