# HG changeset patch
# User kleing
# Date 1052482084 -7200
# Node ID 93769c6c85d79dfc7e0f63fa0a36b0aa5b341dda
# Parent  b289ab046d3b6ea2021e2ee4ab7b56f054bc93f3
fixes

diff -r b289ab046d3b -r 93769c6c85d7 Admin/isatest-check
--- a/Admin/isatest-check	Fri May 09 12:08:00 2003 +0200
+++ b/Admin/isatest-check	Fri May 09 14:08:04 2003 +0200
@@ -58,13 +58,13 @@
 
 # check if tests are still running, wait for them to finish for max 10h
 i=0
-while [ -n $(ls $RUNNING) -a $((i < 10)) ]; do 
+while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
     sleep 3600
-    $((i = i+1))
+    let "i = i+1"
 done
 
 # still running -> give up
-if [ -n $(ls $RUNNING) ]; then
+if [ -n "$(ls $RUNNING)" ]; then
     echo "giving up waiting for test to finish at $(date)" > $TMP
     echo >> $TMP
     echo "Have a nice day," >> $TMP
@@ -79,15 +79,17 @@
 
 # no tests running, check if there were errors
 if [ -e $ERRORLOG ]; then
-  cat $ERRORLOG > $TMP
-	echo "Have a nice day," >> $TMP
-	echo "  isatest" >> $TMP
+    cat $ERRORLOG > $TMP
+    echo "Have a nice day," >> $TMP
+    echo "  isatest" >> $TMP
 
-  for R in $MAILTO; do
-	    $MAIL "isabelle test failed" $R $TMP
-	done
+    for R in $MAILTO; do
+        $MAIL "isabelle test failed" $R $TMP
+    done
 
-	rm $TMP
+    rm $TMP
+    exit 1
 fi
 
+exit 0
 ## end