Hi All - What is the process of closing out pull requests on GitHub for extensions we maintain? For example: https://github.com/php/pecl-numbers-bitset/issues/11 - I have no way of closing that out other than to push a bogus commit with "Fix #11" as the message.
Is there are grant option for GitHub extension maintainers? If so, both PHP and GH username is willfitch. Thanks, Will Fitch
