--- a/Admin/isatest/isatest-makedist Thu Oct 09 08:47:28 2008 +0200
+++ b/Admin/isatest/isatest-makedist Thu Oct 09 09:18:32 2008 +0200
@@ -67,7 +67,7 @@
then
echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
- echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+ log "dist build FAILED, elapsed time $ELAPSED."
echo "Could not build isabelle distribution. Log file available at" > $TMP
echo "$HOSTNAME:$DISTLOG" >> $TMP
@@ -87,7 +87,7 @@
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
+log "dist build successful, elapsed time $ELAPSED."
## clean up var/running
rm -f $RUNNING/*