Tiny tweak for `$header` initialization, it should always be an array

diff --git a/run-tests.php b/run-tests.php
index 1639db5b2536b92f2a0638395635458e5a8d28fe..24e127eec4cc6f965a069d8a66a0fd19923eb247 100755 (executable)
--- a/run-tests.php
+++ b/run-tests.php
@@ -1900,12 +1900,11 @@ COMMAND $cmd
        $output = preg_replace("/\r\n/", "\n", trim($out));
 
        /* when using CGI, strip the headers from the output */
-       $headers = "";
+       $headers = array();
 
        if (isset($old_php) && preg_match("/^(.*?)\r?\n\r?\n(.*)/s", $out, $match)) {
                $output = trim($match[2]);
                $rh = preg_split("/[\n\r]+/", $match[1]);
-               $headers = array();
 
                foreach ($rh as $line) {
                        if (strpos($line, ':') !== false) {