Re: [sage-devel] Accidential push to develop
Thanks Dima for cleaning up my mess. Next time I'll not use git when lying in the bed with a flu ;-) I guess the problem with the branch protection rules is that they actually don't apply to maintainers because of " Do not allow bypassing the above settings" is disabled. Not sure if we can enable that though, or if it would lead to problems with Volker's workflow (we should really look into completely switching to github-based merging) On Tuesday, November 14, 2023 at 6:28:14 PM UTC+8 Dima Pasechnik wrote: > 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 wrote: > > > > On Tue, Nov 14, 2023 at 9:29 AM tobia...@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+...@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/59f36d60-2925-4b86-a9b4-7e8192ded8bcn%40googlegroups.com.
Re: [sage-devel] Accidential push to develop
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 wrote: > > On Tue, Nov 14, 2023 at 9:29 AM tobia...@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.
Re: [sage-devel] Accidential push to develop
On Tue, Nov 14, 2023 at 9:29 AM tobia...@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.
