[dmd-internals] Fixing github pull requests that I borked up

[Walter Bright]

On 10/8/2013 12:06 AM, Jacob Carlborg wrote:
> On Oct 07, 2013, at 09:44 PM, Walter Bright <walter at digitalmars.com> 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.