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