Fix treatment of timeouts in run-tests and pintos.

diff --git a/grading/vm/run-tests b/grading/vm/run-tests
index 85164aa28bbdc94fa8a072c929d22d943484b15d..61adbaf2fdb8c5548d553e9c2198ab38c6d874a6 100755 (executable)
--- a/grading/vm/run-tests
+++ b/grading/vm/run-tests
@@ -696,8 +696,15 @@ sub xsystem {
     };
     if ($@) {
        die unless $@ eq "alarm\n";   # propagate unexpected errors
-       print "Timed out $pid.\n";
-       kill ('SIGTERM', $pid);
+       print "Timed out: ";
+       for (my ($i) = 0; $i < 10; $i++) {
+           kill ('SIGTERM', $pid);
+           sleep (1);
+           my ($retval) = waitpid ($pid, WNOHANG);
+           last if $retval == $pid || $retval == -1;
+           print "Waiting for $pid to die" if $i == 0;
+           print ".";
+       }
        $status = 0;
     }