Thanks, Johannes. I’ve closed that issue out. Please feel free to turn issues
off when you’re able!
> On Oct 7, 2017, at 7:45 AM, Johannes Schlüter wrote:
>
>> On Fr, 2017-10-06 at 20:11 +0200, Christoph M. Becker wrote:
>>
>> Not sure about issues, though. Probably these shouldn't even be
>>
On Fr, 2017-10-06 at 20:11 +0200, Christoph M. Becker wrote:
> Not sure about issues, though. Probably these shouldn't even be
> available.
>
Correct, usually we disable issues and point users to bugs.php.net to
have a central bug database instead of having to track multiple
trackers. Usually
On 06.10.2017 at 19:26, Will Fitch wrote:
> 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
> m
