Re: bad git pull
From: Junio C Hamano <hidden>
Date: 2016-06-15 22:42:15
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.