GitHub has added a new setting to restrict who can create a branch matching a specific name pattern. I've enabled it with *
. If I read the documentation correctly, this should not affect in any way the rules currently in place for master and v... branches. However, it should prevent anyone but the core devs to create any new branch.
This should prevent accidental branch creation by people who are part of the @coq/contributors but are not core devs. Unfortunately, there is no way to extend this restriction to repository admins.
cool
so another interpretation: you now have to be a core dev to submit your PR from an in-repo branch
Yes, but this was always disallowed in the guidelines (including for core devs).
Last updated: Oct 13 2024 at 01:02 UTC