Re: Easy Non-Fast-Forward Pushes

[Junio C Hamano <gitster@pobox.com>]

Lasse Kliemann <lasse@lassekliemann.de> writes:

> 1. Try pushing to origin/master. If it works, fine. If not, goto 2.
>
> 2. Push to the appropriate personal branch.

I wonder what happens to this user _after_ that change gets
integrated on the project side.  Presumably somebody picks up the
change from the "personal branch", does necessary merge and updates
the master, so the next time "git pull" is done, it will
fast-forward?

I have a feeling that running trivial merges on the server-side when
a push is made, and immedately pulling that result back might help
such userbase who does not care too much about the history better,
instead of using the bare-metal 'git pull' and 'git push'.  You'd be
scripting on the client side to do the above two steps for your end
users anyway, so it would not be too much of a stretch to make that
script a bit smarter still?