Stream: Coq devs & plugin devs

Topic: Protecting branch creation


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 01 2022 at 12:44):

cool

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Sep 01 2022 at 13:44):

Yes, but this was always disallowed in the guidelines (including for core devs).


Last updated: Feb 06 2023 at 00:03 UTC