Merging the pull request, to get the commit in. If there is anything else to be sorted out, a new issue can be created.

—
Reply to this email directly or view it on GitHub.