Admin/isatest-makeall
changeset 15888 64533471eec4
parent 14981 e73f8140af78
child 16095 f6af6b265d20
--- 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