multiple merge requests

[Thomas Lange <lange@cs.uni-koeln.de>]

Hi Szabolcs,

I wonder why you do these git merges like
1fdb8a1e721dc37af1a59beb2ca7ce1e07406940
cd07919182802be69fd700d91da1c18de38cba20

and many more? I'm not a git expert, but I guess you can omit this
merge when you rebase your local branch before pushing.

regards Thomas