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
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).
that rule only applies to master no release branches
doing the change now
Right, anyway, pushers already didn't have permissions on branches other than master.
Last updated: Oct 13 2024 at 01:02 UTC