JSON: fix config.w32 / Install headers on windows

diff --git a/NEWS b/NEWS
index 5085cb108d1e171fa647a48e4304d462f185d3d7..7ff084990188b97d5a08eec35c6f89035d024ccc 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -578,6 +578,7 @@ PHP                                                                        NEWS
 
 - JSON:
   . Fixed bug #73526 (php_json_encode depth issue). (Jakub Zelenka)
+  . Install headers on windows. (Darek Slusarczyk)
 
 - Mysqlnd:
   . Fixed bug #64526 (Add missing mysqlnd.* parameters to php.ini-*). (cmb)

diff --git a/ext/json/config.w32 b/ext/json/config.w32
index c37d9a9025edac26aae68bbc3399e33f97026e91..c1a8ccfb3061449de4d7c8bc63bdd3e5551424cc 100644 (file)
--- a/ext/json/config.w32
+++ b/ext/json/config.w32
@@ -17,6 +17,6 @@ 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");
+       PHP_INSTALL_HEADERS("ext/json/", "php_json.h php_json_parser.h php_json_scanner.h");
 }