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

[Leandro Lucarella]

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.

-- 
Leandro Lucarella (AKA luca)                     http://llucax.com.ar/
----------------------------------------------------------------------
GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145  104C 949E BFB6 5F5A 8D05)
----------------------------------------------------------------------
Americans, let's face it: We've been a spoiled country for a long time.
Do you know what the number one health risk in America is?
Obesity, obesity! They say we're in the middle of an obesity epidemic.
An epidemic, like it's polio. Like we'll be telling our grand kids about
it one day: The Great Obesity Epidemic of 2004.
"How'd you get through it grandpa?"
"Oh, it was horrible Johnny, but there was cheesecake
and pork chops everywhere."