# HG changeset patch
# User kleing
# Date 1114774555 -7200
# Node ID 64533471eec43bf430b87fe4068ccc72c5491b7c
# Parent  7dee3396d8b04bc9253670e25d2729b8dca7739e
put 8h time limit on test

diff -r 7dee3396d8b0 -r 64533471eec4 Admin/isatest-makeall
--- a/Admin/isatest-makeall	Fri Apr 29 13:12:38 2005 +0200
+++ b/Admin/isatest-makeall	Fri Apr 29 13:35:55 2005 +0200
@@ -19,6 +19,8 @@
 # where to put test-is-running files
 RUNNING=$HOME/var/running
 
+# max time until test is aborted (in sec)
+MAXTIME=28800
 
 ## diagnostics
 
@@ -108,7 +110,7 @@
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
+    (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then