Admin/isatest/isatest-annomaly

--- a/Admin/isatest/isatest-annomaly	Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-annomaly	Thu Oct 09 09:18:32 2008 +0200
@@ -34,7 +34,7 @@
 function fail()
 {
   echo "$1" >&2
-  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+  log "FAILED, $1"
   exit 2
 }
 
@@ -89,4 +89,4 @@
 # grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
 
 
-echo "$(date) $HOSTNAME $PRG: annomaly docs generated successfully." >> $MASTERLOG
+log "annomaly docs generated successfully."