Stream: Coq devs & plugin devs

Topic: master merging rules


view this post on Zulip Gaëtan Gilbert (Jun 20 2024 at 12:19):

should we remove pushers from allowed in https://github.com/coq/coq/settings/rules/3041
to prevent merging by pushing the github button like happened to https://github.com/coq/coq/pull/19248

view this post on Zulip Théo Zimmermann (Jun 20 2024 at 12:21):

I'm fine with the proposed change. Note that this means they no longer can use the merge script, but I think almost no one uses it anymore (except release managers for release branches).

view this post on Zulip Gaëtan Gilbert (Jun 20 2024 at 12:22):

that rule only applies to master no release branches

view this post on Zulip Gaëtan Gilbert (Jun 20 2024 at 12:22):

doing the change now

view this post on Zulip Théo Zimmermann (Jun 20 2024 at 12:23):

Right, anyway, pushers already didn't have permissions on branches other than master.


Last updated: Oct 13 2024 at 01:02 UTC