terminate timeouting processes with SIGKILL (9)

diff --git a/run-tests.php b/run-tests.php
index a615efccdcff8d862533c5c0d37c242e2a7d20c5..ddd1f5f494a425f484fddcfe31e1f6a9ee3fa34b 100755 (executable)
--- a/run-tests.php
+++ b/run-tests.php
@@ -1082,7 +1082,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);