Thanks. Done in commit 4d31c5bd4f3a45.
<OT>
Hint: If you or anybody else want to send a patch with a commit message
and your own author you can do the following:
1) make sure your repo is up-to-date (`git checkout master; git pull`)
2) check out a working branch (`git checkout -b working`)
3) change code and commit your changes
4) create patch file(s): `git format-patch master..`
Note the trailing '..' !
This will create one or more patch files with names like
'nnnn-Commit-Message-Title.patch where 'nnnn' is a sequence number. Then
attach the patch file(s) to the message.
To clean up your repo:
5) git checkout master
6) git branch -D working
Note the uppercase 'D' to delete the unmerged branch.
Such patch files can be applied with `git am 000*.patch` in sequence and
with the original time stamp and author.
Of course this is not necessary, I can also apply the patch as it was
pasted in the message text. This hint is just in case someone wants to
send in a patch and keep their author and commit messages.
I put this on my todo list for the appropriate article.
</OT>