Jonathan M Davis, el  9 de October a las 14:20 me escribiste:
> On Wednesday, October 09, 2013 19:48:48 David Nadlinger wrote:
> > On Mon, Oct 7, 2013 at 9:44 PM, Walter Bright <walter@digitalmars.com>
> wrote:
> > > Git, miserable program that it is, has no:
> > > git undo
> > 
> > Actually it does, sort of, but only for local changes: There is "git reflog", which lists all the different locations your HEAD pointed to, and "git reset --hard HEAD@{1}" resets your branch to where it pointed before the last operation.
> > 
> > This is more of a handy trick if you know what you are doing than a fail-safe undo feature though.
> 
> Though to be honest, I don't think that anyone should be messing around with resets (especially hard resets) without fully understanding what they're doing. git reset is a very handy feature to be sure, but it also makes it very easy to lose commits if you're not careful.

You never really lose commits until the GC runs, which by default
I think it doesn't remove anything newer than 90 days. So that's what
reflog is good for, finding commits you missed some way or another, but
are still present in the git object database.

-- 
Leandro Lucarella (AKA luca)                     http://llucax.com.ar/
----------------------------------------------------------------------
GPG Key: 5F5A8D05 (F8CD F9A7 BF00 5431 4145  104C 949E BFB6 5F5A 8D05)
----------------------------------------------------------------------
22% of the time a pizza will arrive faster than an ambulance in
Great-Britain
_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

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
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals