On 10/8/13 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.
Completely agreed.
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.
The fix was merely repushing the commit id of the previously head of master back as the current head
of master. Something internal to github's management of pulls got confused at that point. So far,
no response to my support request.
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
