Merged (see commit 00c7b9dbfcef38ce6a8369ba1593f11b806a061f). Thanks for the report and the pull request!