[Dune-devel] Please use git rebase

[Christoph Grüninger]

Hi Dune developers,
could I kindly ask to please, pretty please with sugar on top, use git
rebase before pushing your changes to the repositories? For me it is
really annoying to have so many useless merge commits. There are cases
were merges cannot be avoided, but in majority it could be rebased
without a hassle.

Here a brief how-to:
> git commit
> git pull
(ok, something changed, you have to merge and commit this merge. Now
come you:)
> git rebase origin/master
(merge vanishes)
> git push
(et voilà, you just got rid of the merge)

Thank you in advance
Christoph

-- 
Une science n'était vraiment développée que quand elle
pouvait utiliser les mathématiques.    (Paul Lafargue)
*********************************************
CMWR 2014: 10th - 13th June 2014 in Stuttgart
         Please visit www.cmwr14.de
*********************************************