--- a/Admin/isatest/isatest-check Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-check Thu Oct 09 09:18:32 2008 +0200
@@ -98,9 +98,9 @@
# (failures in experimental sessions ok)
if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
(cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
- echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+ log "generated development snapshot web page."
else
- echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
+ log "test failures, no web snapshot generated."
fi
exit 0