An example:
https://github.com/D-Programming-Language/dmd/pull/2615
See all those extra commits in there? That's because I did a:
git push -f
from the wrong branch. Git, miserable program that it is, has no:
git undo
which it so desperately needs. Anyhow, this royally borked up github. Brad
Roberts came riding the rescue, and got the damage to the main repo undone.
However, the PR's did not fix themselves.
However, I discovered that if I:
git checkout myfixbranch
git commit --amend -a
git push -f
for my PR's, one by one, it fixed the PR's. So I fixed mine, but y'all will
likely each have to fix yours one by one. Brad has an email in to github support
to see if this can be fixed without needing each of us to do it, but in the
meantime, or if that doesn't pan out, this should work.
Sorry about this.
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
