On 18 September 2017 at 19:04, Dmitry Stogov <dmi...@zend.com> wrote:
> This commit should fix the problem https://github.com/php/php-src/commit/ > 5ef10d08ec2d0823fb21ad189dacfb43d900a0b5 > > > Yes! I tested 7.2.0RC2 with this patch applied and it fixes the problem. Thank you!