Théo Zimmermann (Sep 01 2022 at 12:35): Théo Zimmermann (Sep 01 2022 at 12:35):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.
Théo Zimmermann (Sep 01 2022 at 12:39):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.
Gaëtan Gilbert (Sep 01 2022 at 12:44):cool
Karl Palmskog (Sep 01 2022 at 12:46):so another interpretation: you now have to be a core dev to submit your PR from an in-repo branch
Théo Zimmermann (Sep 01 2022 at 13:44):Yes, but this was always disallowed in the guidelines (including for core devs).
Last updated: Apr 20 2024 at 13:01 UTC