Pull-Request has been merged by copperi
Thank you! As specified in the readme, anybody whose pull request is approved is granted committer access. In the future, you can directly commit such trivial fixes. Pull requests are still preferred for changes that may create discussion.