Admin/isatest/isatest-doc

 ## 
 
 [ "$#" != "0" ] && usage
 
 if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
-  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
+  log "Skipped test. Isabelle devel version broken."
   exit 1
 fi
 cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
 
 

 # send email if there was a problem
 if [ "$FAIL" != "" ]; then
   echo >> $LOG
   echo "Failed sessions: ${FAIL}" >> $LOG
 
-  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
+  log "doc test FAILED for ${FAIL}, elapsed time $ELAPSED."
 
   cat > $TMP <<EOF
 Session(s) ${FAIL} in the documentation test failed (log attached).
 Test ended on: $HOSTNAME, `date`.
 

 
   rm -f $TMP
 
   exit 1
 else
-  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
+  log "doc test successful, elapsed time $ELAPSED."
 fi