On 10/8/2013 12:06 AM, Jacob Carlborg wrote:
On Oct 07, 2013, at 09:44 PM, Walter Bright <[email protected]> wrote:
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
Why did you do a force push in the first place? If you can't push, you
shouldn't just blindly add "-f" to force the push. You should stop and think
of why you can't push it without force in the first place. You need to stop
doing this. No offense, but you obviously can not completely handle git.
Either learn how to handle it or ask some one, BEFORE you're doing something
like this.
Because I often need to amend a pull request, and I was told it was done with:
git --amend -a
git push -f
and I've been doing that successfully since I've been doing PR's.
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.
I don't know what exactly had happened or how Brad "fixed" this, but I'm
pretty sure it's possible to correctly fix this without breaking the pull
requests. Just reset back the history to the sate it was before the force
push. Since you already made a push force, another push force is needed to fix
the problem. Then correctly make the changes you wanted to make.
Brad used a git reset followed by a git push with -f. The github master is now
correct, but it's a mystery why the PR's are messed up.
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
