Thanks, Philipp, I've just pushed a release with this patch.
[ For reference, diff -u is slightly nicer; even better, a git
format-patch would have helped getting proper authoring info to be
directly recorded into git. ]
Thanks a lot for fixing this so fast.
Actually I wanted to submit a git diff, but I could not figure out where the repository can be found. I have found it now, though :)