On Wed, Apr 13, 2011 at 08:24:32PM +0200, Georg Brandl wrote:
summary: merge from push conflict.
this message is not quite correct -- there is no conflict involved. You're just merging two heads on the same branch in order to have only one head in the master repo.
Okay, got it. I should have just said merge. (I probably typed push conflict, because push was not allowed as some had already pushed to repo in quick succession), it is just a merge.