# HG changeset patch
# User wenzelm
# Date 935059382 -7200
# Node ID bb9502f9154a0c85bfd5e1bd57cad4546bf4bb3f
# Parent  7a2008de228dc05304c6687f778b0c366d404282
improved messages;

diff -r 7a2008de228d -r bb9502f9154a build
--- a/build	Thu Aug 19 12:42:43 1999 +0200
+++ b/build	Thu Aug 19 12:43:02 1999 +0200
@@ -106,6 +106,7 @@
   echo "  ML_SYSTEM=$ML_SYSTEM"
   echo "  ML_HOME=$ML_HOME"
   echo "  ML_OPTIONS=$ML_OPTIONS"
+  echo "  ML_PLATFORM=$ML_PLATFORM"
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
 fi
@@ -154,7 +155,9 @@
 # build it
 
 SECONDS=0
-echo -n "Started at "; date
+DATE=$(date)
+HOST=$(hostname)
+echo "Started at $DATE ($HOST)"
 
 export THIS_IS_ISABELLE_BUILD=true
 
diff -r 7a2008de228d -r bb9502f9154a lib/Tools/makeall
--- a/lib/Tools/makeall	Thu Aug 19 12:42:43 1999 +0200
+++ b/lib/Tools/makeall	Thu Aug 19 12:43:02 1999 +0200
@@ -30,7 +30,9 @@
 
 
 SECONDS=0
-echo -n "Started at "; date
+DATE=$(date)
+HOST=$(hostname)
+echo "Started at $DATE ($HOST)"
 
 for L in $ALL_LOGICS
 do
diff -r 7a2008de228d -r bb9502f9154a src/Pure/mk
--- a/src/Pure/mk	Thu Aug 19 12:42:43 1999 +0200
+++ b/src/Pure/mk	Thu Aug 19 12:43:02 1999 +0200
@@ -80,7 +80,7 @@
 
 if [ -z "$RAW" ]; then
   ITEM="Pure"
-  echo -n "Building $ITEM ..."
+  echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -90,7 +90,7 @@
   RC=$?
 else
   ITEM="RAW"
-  echo -n "Building $ITEM ..."
+  echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -106,10 +106,9 @@
 # exit status
 
 if [ $RC -eq 0 ]; then
-  echo " OK  ($ELAPSED elapsed time)"
+  echo "Finished $ITEM ($ELAPSED elapsed time)"
   gzip --force "$LOG"
 else
-  echo
   echo "$ITEM FAILED"
   echo "(see also $LOG)"
   echo; tail $LOG; echo