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
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
