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