If you chose to submit the pull request instead, keep in mind that we are not checking on them regularly, so it might take ages before we even get to it, if at all.
Unfortunately, GitHub does not allow us to disable the pull requests feature for this repository, so we have to warn you this way...