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