terminate timeouting processes with SIGKILL (9)

diff --git a/run-tests.php b/run-tests.php
index bc5f99bc0971e066df90df2e8dd208444c156dce..4bd154611866d3f60426d9c7478ec24fef8681e1 100755 (executable)
--- a/run-tests.php
+++ b/run-tests.php
@@ -1080,7 +1080,7 @@ function system_with_timeout($commandline, $env = null, $stdin = null)
                } else if ($n === 0) {
                        /* timed out */
                        $data .= b"\n ** ERROR: process timed out **\n";
-                       proc_terminate($proc);
+                       proc_terminate($proc, 9);
                        return $data;
                } else if ($n > 0) {
                        $line = (binary) fread($pipes[1], 8192);