From: Ben Pfaff <blp@cs.stanford.edu>
Date: Mon, 7 Feb 2005 05:52:50 +0000 (+0000)
Subject: Increase default timeout to 15 seconds.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=39c5d0ad729238d08668ce0eeaa71bc25540bc7b;p=pintos-anon

Increase default timeout to 15 seconds.
---

diff --git a/grading/threads/run-tests b/grading/threads/run-tests
index 731499a..0852f6f 100755
--- a/grading/threads/run-tests
+++ b/grading/threads/run-tests
@@ -94,7 +94,7 @@ sub run_test {
     xsystem ("cp pintos/src/threads/build/os.dsk output/$test");
 
     # Run.
-    my ($timeout) = $test !~ /^mlfqs/ ? 10 : 600;
+    my ($timeout) = $test !~ /^mlfqs/ ? 15 : 600;
     return run_pintos (["-v", "run", "-q"],
 		       CHDIR => "pintos/src/threads/build",
 		       LOG => "$test/run",