Fix #63362: Not needed but installed headers#3937

petk wants to merge 1 commit intophp:PHP-7.2php/php-src:PHP-7.2from

petk:patch-fix-63362petk/php-src:patch-fix-63362Copy head branch name to clipboard