# HG changeset patch
# User wenzelm
# Date 935059269 -7200
# Node ID 3a001f2148f7391666a63e0c4a870ae6841c126d
# Parent  3635733a9291bede21532cd8b9180aa9dde3a1dc
removed -m option;

diff -r 3635733a9291 -r 3a001f2148f7 lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Aug 19 12:39:19 1999 +0200
+++ b/lib/Tools/usedir	Thu Aug 19 12:41:09 1999 +0200
@@ -126,12 +126,9 @@
 
 PARENT=$(basename "$LOGIC")
 
-ECHO_LINE="echo -n"
-[ "$MULTI" = "true" ] && ECHO_LINE="echo"
-
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
-  $ECHO_LINE "Building $ITEM ..."
+  echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -140,7 +137,7 @@
   RC=$?
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
-  $ECHO_LINE "Running $ITEM ..."
+  echo "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   cd "$NAME"
@@ -157,14 +154,9 @@
 # exit status
 
 if [ $RC -eq 0 ]; then
-  if [ "$MULTI" = "true" ]; then
-    echo "Finished $ITEM  ($ELAPSED elapsed time)"
-  else
-    echo " OK  ($ELAPSED elapsed time)"
-  fi
+  echo "Finished $ITEM ($ELAPSED elapsed time)"
   gzip --force "$LOG"
 else
-  [ "$MULTI" = "true" ] || echo
   echo "$ITEM FAILED"
   echo "(see also $LOG)"
   echo; tail $LOG; echo