Johannes Schindelin <Johannes.Schindelin@gmx.de> writes:

quoted text
> 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.

*DANGER*

A pull is usually just a fetch and a merge, but sometimes it can
fast forward.  ORIG_HEAD, not HEAD^, points at the previous HEAD
location in both cases.

-
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html