Accidential push to develop

[Tobia...@gmx.de]

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?

[Dima Pasechnik]

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.

[Dima Pasechnik]

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_

[Tobia...@gmx.de]

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)