Re: git pull opinion

Hi,

On Mon, 5 Nov 2007, Aghiles wrote:

quoted

The consense was that you are much better off committing first, then 
pulling.  And if the work you are doing really is not committable, but 
you _have_ to pull _now_, you use stash.  Although you are quite 
likely to revert the pull when it succeeds, and _then_ unstash.

Sorry but I don't really understand why one should "revert the pull" ? 
Could elaborate for a newbie ? :)

Yes, no problem.

A pull is just a fetch and a merge.  And a merge is a commit with more 
than one parent.  So you can use the command "git reset --hard HEAD^" to 
undo a merge, just as you can undo any other commit.

NOTE: if you pushed that commit (merge or not), do _not_ use reset.  This 
effectively rewrites history, and _will_ upset people pulling from you.  
If you really have to undo a commit you already published, use "git revert 
<commit>".

Hth,
Dscho