From: Ben Pfaff 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=60340711d147c11cd2c70c0d50b6509f498ae1fc;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",