Hi, On Tue, 6 Nov 2007, Junio C Hamano wrote: > Johannes Schindelin <Johannes.Schindelin@xxxxxx> 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. Oops. Right. Thanks, Dscho - To unsubscribe from this list: send the line "unsubscribe git" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
