Hi, I took the liberty to fix the develop branch by force-pushing 10.2.rc2 branch. All should be in order now, and PRs can proceed.
A copy of the accidentally pushed to develop is here: https://github.com/dimpase/sage/tree/develop_accidentally_pushed_to_ On Tue, Nov 14, 2023 at 9:43 AM Dima Pasechnik <dimp...@gmail.com> wrote: > > 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/CAAWYfq278D-1sp8vjb27Q-aw4-PQgARDp%3DZu4jBEQFKpV9VbOg%40mail.gmail.com.
