Merge branch 'PHP-7.1' into PHP-7.2

# Conflicts:
#	ext/json/config.w32

diff --cc ext/json/config.w32
index 05f6e659e42659a174f46e01015c792b797f87dd,c1a8ccfb3061449de4d7c8bc63bdd3e5551424cc..d16e0686d3bc32f431c19909bec1524719d4cfb2
--- 1/ext/json/config.w32
--- 2/ext/json/config.w32
+++ b/ext/json/config.w32
@@@ -17,8 -17,6 +17,8 @@@ if (PHP_JSON != "no") 
  
        ADD_SOURCES(configure_module_dirname, "json_encoder.c json_parser.tab.c json_scanner.c", "json");
  
-       PHP_INSTALL_HEADERS("ext/json/", "php_json.h");
 +      ADD_MAKEFILE_FRAGMENT();
 +
+       PHP_INSTALL_HEADERS("ext/json/", "php_json.h php_json_parser.h php_json_scanner.h");
  }