I didn’t think this was even possible, but I did it:
~/cmdstan/stan/lib/stan_math(develop)$ git commit -a -m "refactor, doc, replace const T with const T&"
[develop 4d7a8f2] refactor, doc, replace const T with const T&
29 files changed, 215 insertions(+), 277 deletions(-)
rewrite stan/math/prim/mat/err/check_ldlt_factor.hpp (67%)
rewrite stan/math/prim/mat/fun/rank.hpp (76%)
~/cmdstan/stan/lib/stan_math(develop)$ git push
Counting objects: 85, done.
Delta compression using up to 8 threads.
Compressing objects: 100% (47/47), done.
Writing objects: 100% (47/47), 10.27 KiB, done.
Total 47 (delta 32), reused 0 (delta 0)
remote: Resolving deltas: 100% (32/32), completed with 30 local objects.
6f02a99..4d7a8f2 develop -> develop
Now the question is how to I undo that magic?
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
OK, did this:
git revert 4d7a8f2
where the SHA 4d7a8f2 is the has for the bad commit. I think that worked. Could someone just please check my work? Thanks.
Our messages crossed! Thanks. That seems to have worked.
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.
I think what you did worked.
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 possible set permissions so that also admins are restricted pushing directly and required to make pull requests
Not on a per-user basis. I believe @seantalts is making the upstream
merging happening by using the ability to merge directly.
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.
Bob, you’re no longer an “owner.” That’ll prevent a push.