# HG changeset patch
# User wenzelm
# Date 1167944326 -3600
# Node ID 3d4ea1819cb76116e1e24340ee4d11dda1f6bed0
# Parent  f3d550d2b145100300a585150a225d9295734602
tuned msg;

diff -r f3d550d2b145 -r 3d4ea1819cb7 src/Pure/mk
--- a/src/Pure/mk	Thu Jan 04 21:37:02 2007 +0100
+++ b/src/Pure/mk	Thu Jan 04 21:58:46 2007 +0100
@@ -96,7 +96,7 @@
   RC="$?"
 elif [ -n "$RAW_SESSION" ]; then
   ITEM="RAW-$(basename $(dirname "$RAW_SESSION"))"
-  echo "Building $ITEM ..."
+  echo "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \