mirror of
https://github.com/php/php-src.git
synced 2026-03-30 12:13:02 +02:00
Thanks to Ilija Tovilo for noticing and reporting this problem. Thanks also to Michael Voříšek for finding the StackOverflow post which explained the reason for the failure.