Re: git pull opinion
- From
Junio C Hamano <gitster@pobox.com>
- Date
- Nov 6, 2007, 18:13 UTC
- 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.