Hey Internals, Sorry if this isn't the correct thing to do, I was just hoping to raise some awareness for a PR I opened last year: https://github.com/php/php-src/pull/1280
It's a very simple and small addition, is it possible get it merged for 7.2, or do I need to raise an RFC for it? Thanks, Craig
