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

[Brad Roberts]

On 10/9/13 3:38 AM, Leandro Lucarella wrote:
> Brad Roberts, el  8 de October a las 01:26 me escribiste:
>>> 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.
>
> GitHub support is pretty crappy, at least according to my experience.
> I had a couple of very strange situations too, where things that
> shouldn't had happened, happened. And I never got an useful answer or
> explanation from them.

At least in this case, they're being helpful, if a little slower than I'd hoped for.  The pull 
request I gave them to use as a representative example got merged by Andrei.  Their first cleaned up 
pull looks good, but it's old enough that it has a merge conflict.  I just gave them another to 
confirm that their cleanup works which was mergeable before the screw-up and still is.  Assuming it 
is after they clean up that pull they'll do the rest for us.  Presumably they'll fix the underlying 
bug too, and I'll follow up on that once we're back in pre-event shape.

More soon,
Brad