X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=grading%2Fvm%2Frun-tests;h=61adbaf2fdb8c5548d553e9c2198ab38c6d874a6;hb=538e0cc1951cc2edf253918fd83fc3c36d9a6398;hp=85164aa28bbdc94fa8a072c929d22d943484b15d;hpb=625ab3a2022422b65f32e73b2c99446b614940de;p=pintos-anon

diff --git a/grading/vm/run-tests b/grading/vm/run-tests
index 85164aa..61adbaf 100755
--- 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;
     }