Re: bad git pull

Nicolas Pitre [off-list ref] writes:

quoted

I do not see much difference either way,

ORIG suggests "origin" to me,...

Hmph.

I always thought it was original-head before the operation
happened, which is why I said it is no different from
previous-head.