I would try to finagle it back myself, but as some of you may have witnessed in the past, I’m not very good at understanding instructions from the web on GitHub. If someone could just undo this push for me, I’d be most grateful.
On public branches we just want to revert something like this. I’ll take care of it. I think it’ll just be a git revert 4d7a8f2; git push origin develop
But now how do I get all my changes back? I didn’t want to erase all my work. I want to keep going and put all the work I accidentally pushed onto a branch and then save it.
Now to keep working on it, check out your development branch (or make one) and revert the revert commit (git revert ba1f8a0bcff86452e100f773c4f0f735842766ff). I realize that sounds a little silly but append-only is the way to go here.
@Bob_Carpenter, I think we can change your permissions on GitHub so you don’t have permissions to push. It may require you not being an admin, but I think as there are a few of us with admin privileges, there’s no need to also have you as admin. Let me or maybe @seantalts know if you would prefer that.
It’s actually organization owners who aren’t restricted. I think the release functionality was also much easier with owners being excluded from those restrictions.