I pushed the patch manually, with you as author -- the commit message was not appropriate for the changelog style, changed that to something more human friendly.

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