Thank you. I have merged it to git master, after reformatting the git commit message a bit. You can find the preferred format in the CONTRIBUTING document.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.