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

[Brad Roberts]

On 10/10/13 9:48 AM, Brad Roberts wrote:
> 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.

Ok, all of the remaining dmd pull request should be cleaned up.  I haven't checked them all, but did 
some spot checking.