Re: Recording the date at which a change was pushed to Savannah

[Eli Zaretskii]

> From: Stefan Monnier <address@hidden>
> Cc: address@hidden,  address@hidden
> Date: Wed, 03 Dec 2014 16:10:30 -0500
> 
> > But in any case, no matter how the mainline became one, it is still
> > _the_ mainline, right?
> 
> No, in the above example, the commit that was the head of the remote
> branch before the "git push" (and was hence obviously on "the" mainline)
> is not in "the" mainline after the "git push".

Yes, but that's just means the mainline moved.  It will still be shown
the same to you and me, right?