Thanks! I pushed the commit manually with you as author to get rid of extra merge pull request notification, but also follow the commit message guidelines for formatting (which I forgot to point to previously):

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