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.