# HG changeset patch
# User isatest
# Date 1024666759 -7200
# Node ID 568bc754d303f30e9e55fef060faee248873d0dd
# Parent  c26fc3baeffc7d3fc6082bd4c8c86fb653e2ee32
included masterlog file

diff -r c26fc3baeffc -r 568bc754d303 Admin/isatest-makeall
--- a/Admin/isatest-makeall	Fri Jun 21 12:35:33 2002 +0200
+++ b/Admin/isatest-makeall	Fri Jun 21 15:39:19 2002 +0200
@@ -10,6 +10,8 @@
 ## global settings
 LOGPREFIX=~/log
 
+MASTERLOG=$LOGPREFIX/isatest.log
+
 ## diagnostics
 
 PRG="$(basename "$0")"
@@ -64,15 +66,24 @@
 
     if [ $? -eq 0 ]
     then
-        echo ------------------- test successfull --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
-        mv $DISTPREFIX/Isabelle/etc/settings-$SHORT $DISTPREFIX/Isabelle/etc/settings
+        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+        mv $DISTPREFIX/Isabelle/etc/settings.save-$SHORT $DISTPREFIX/Isabelle/etc/settings
         gzip -f $TESTLOG
     else
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+	FAIL="$FAIL$SHORT "
         # more action here
-        exit 1
     fi
 
 done
 
-# end
\ No newline at end of file
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+
+if [ "$FAIL" != "" ]; then
+	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+	exit 1
+else
+        echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
+fi
+
+# end