You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to sage-devel
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
unread,
Nov 14, 2023, 4:44:07 AM11/14/23
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to sage-...@googlegroups.com
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.
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to sage-devel
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)