On Tue, Nov 14, 2023 at 9:29 AM tobia...@gmx.de <tobiasd...@gmx.de> wrote:
>
> Hi everybody,
>
> I just accidentally pushed to the develop branch (instead of to a new branch 
> in my fork). I'm very sorry! I leave it to the release manager to revert/fix 
> it to not introduce more issues.
>
> What confuses me, however, is how this was possible in first place?! I 
> thought we had branch protection rules in place that prevented such things. 
> Did someone recently changed something in these rules?

Maybe github had introduced a bug; anyway, " Restrict who can push to
matching branches " is not
on for develop [1], and  this seems to mean that non-force pushed may
be done by anyone in an appropriate team.

I've switched it on now, for the time being.

(force pushed are limited to Volker)

[1] https://github.com/sagemath/sage/settings/branch_protection_rules/33965567


>
> --
> You received this message because you are subscribed to the Google Groups 
> "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to sage-devel+unsubscr...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/sage-devel/842f9089-e9cc-4c5d-b706-1eefc055e455n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups 
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to sage-devel+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/sage-devel/CAAWYfq3pAAf0M%3D-YJ2U1hF8KtSKqxKfpi%3DWnYjNFUNu4gvpEXg%40mail.gmail.com.

Reply via email to