equal
deleted
inserted
replaced
17 ERRORLOG=$ERRORDIR/error.log |
17 ERRORLOG=$ERRORDIR/error.log |
18 |
18 |
19 # where to put test-is-running files |
19 # where to put test-is-running files |
20 RUNNING=$HOME/var/running |
20 RUNNING=$HOME/var/running |
21 |
21 |
|
22 # max time until test is aborted (in sec) |
|
23 MAXTIME=28800 |
22 |
24 |
23 ## diagnostics |
25 ## diagnostics |
24 |
26 |
25 PRG="$(basename "$0")" |
27 PRG="$(basename "$0")" |
26 |
28 |
106 touch $RUNNING/$SHORT.running |
108 touch $RUNNING/$SHORT.running |
107 |
109 |
108 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
110 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
109 |
111 |
110 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
112 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
111 $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
113 (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1) |
112 |
114 |
113 if [ $? -eq 0 ] |
115 if [ $? -eq 0 ] |
114 then |
116 then |
115 # test log and cleanup |
117 # test log and cleanup |
116 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
118 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |