--- 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