# HG changeset patch
# User wenzelm
# Date 934996649 -7200
# Node ID 2d09363ada6caac8eeb16fdc2d6214b0179cd542
# Parent  a05dc63ca29bdf4f08175708c8c67af5fcfeb55a
tuned messages;

diff -r a05dc63ca29b -r 2d09363ada6c src/Pure/mk
--- a/src/Pure/mk	Wed Aug 18 18:44:20 1999 +0200
+++ b/src/Pure/mk	Wed Aug 18 19:17:29 1999 +0200
@@ -80,7 +80,7 @@
 
 if [ -z "$RAW" ]; then
   ITEM="Pure"
-  echo -n "Building $ITEM ... "
+  echo -n "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -90,7 +90,7 @@
   RC=$?
 else
   ITEM="RAW"
-  echo -n "Building $ITEM ... "
+  echo -n "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -106,10 +106,11 @@
 # exit status
 
 if [ $RC -eq 0 ]; then
-  echo "OK  ($ELAPSED elapsed time)"
+  echo " OK  ($ELAPSED elapsed time)"
   gzip --force "$LOG"
 else
-  echo "FAILED"
+  echo
+  echo "$ITEM FAILED"
   echo "(see also $LOG)"
   echo; tail $LOG; echo
 fi