Allow for special case for the opcache zend extension

derickr · derickr · commit c35bd4861d49 · 2016-05-10T15:40:03.000-04:00
diff --git a/run-tests.php b/run-tests.php
@@ -1547,7 +1547,11 @@ function run_test($php, $file, $env)
 		$loaded = explode(",", `$php -n -r 'echo join(",", get_loaded_extensions());'`);
 		foreach ($extensions as $req_ext) {
 			if (!in_array($req_ext, $loaded)) {
-				$ini_settings['extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;
+				if ($req_ext == 'opcache') {
+					$ini_settings['zend_extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;
+				} else {
+					$ini_settings['extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;
+				}
 			}
 		}
 	}
@@ -2374,7 +2378,7 @@ function settings2array($settings, &$ini_settings)
 			$name = trim($setting[0]);
 			$value = trim($setting[1]);
 
-			if ($name == 'extension') {
+			if ($name == 'extension' || $name == 'zend_extension') {
 
 				if (!isset($ini_settings[$name])) {
 					$ini_settings[$name] = array();

Original file line number	Diff line number	Diff line change
`@@ -1547,7 +1547,11 @@ function run_test($php, $file, $env)`
`1547`	`1547`	$loaded = explode(",", `$php -n -r 'echo join(",", get_loaded_extensions());'`);
`1548`	`1548`	`foreach ($extensions as $req_ext) {`
`1549`	`1549`	`if (!in_array($req_ext, $loaded)) {`
`1550`		`- $ini_settings['extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;`
	`1550`	`+ if ($req_ext == 'opcache') {`
	`1551`	`+ $ini_settings['zend_extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;`
	`1552`	`+ } else {`
	`1553`	`+ $ini_settings['extension'][] = $ext_dir . DIRECTORY_SEPARATOR . $req_ext . '.' . PHP_SHLIB_SUFFIX;`
	`1554`	`+ }`
`1551`	`1555`	`}`
`1552`	`1556`	`}`
`1553`	`1557`	`}`
`@@ -2374,7 +2378,7 @@ function settings2array($settings, &$ini_settings)`
`2374`	`2378`	`$name = trim($setting[0]);`
`2375`	`2379`	`$value = trim($setting[1]);`
`2376`	`2380`
`2377`		`- if ($name == 'extension') {`
	`2381`	`+ if ($name == 'extension' \|\| $name == 'zend_extension') {`
`2378`	`2382`
`2379`	`2383`	`if (!isset($ini_settings[$name])) {`
`2380`	`2384`	`$ini_settings[$name] = array();`