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

[Stefan Monnier]

>> IIRC when you do:
>> 
>> git commit
>> git pull
>> <merge&commit>
>> git push
>> 
>> The merge commit will put what was previously "the mainline" in the
>> "second" position, while your "git commit" will now appear as being on
>> "the mainline".

> That's why we recommend "git pull --rebase" in this case (and I
> actually pull.rebase = preserve in my .gitconfig).

There might also be a way to ask Git to generate the "merge commit" with
its two parent swapped.

> 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".


        Stefan