From: Junio C Hamano <gitster@pobox.com>
Date: Tue, 06 Nov 2007 18:13:22 GMT
Subject: Re: git pull opinion
Message-ID: <7v1wb3i6nx.fsf@gitster.siamese.dyndns.org>
In-Reply-To: <Pine.LNX.4.64.0711061159240.4362@racer.site>

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

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