Lasse Kliemann <lasse@xxxxxxxxxxxxxxxx> 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? -- To unsubscribe from this list: send the line "unsubscribe git" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html