improved messages;
authorwenzelm
Thu, 19 Aug 1999 12:43:02 +0200
changeset 7277bb9502f9154a
parent 7276 7a2008de228d
child 7278 da64f7413efd
improved messages;
build
lib/Tools/makeall
src/Pure/mk
     1.1 --- a/build	Thu Aug 19 12:42:43 1999 +0200
     1.2 +++ b/build	Thu Aug 19 12:43:02 1999 +0200
     1.3 @@ -106,6 +106,7 @@
     1.4    echo "  ML_SYSTEM=$ML_SYSTEM"
     1.5    echo "  ML_HOME=$ML_HOME"
     1.6    echo "  ML_OPTIONS=$ML_OPTIONS"
     1.7 +  echo "  ML_PLATFORM=$ML_PLATFORM"
     1.8    echo
     1.9    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    1.10  fi
    1.11 @@ -154,7 +155,9 @@
    1.12  # build it
    1.13  
    1.14  SECONDS=0
    1.15 -echo -n "Started at "; date
    1.16 +DATE=$(date)
    1.17 +HOST=$(hostname)
    1.18 +echo "Started at $DATE ($HOST)"
    1.19  
    1.20  export THIS_IS_ISABELLE_BUILD=true
    1.21  
     2.1 --- a/lib/Tools/makeall	Thu Aug 19 12:42:43 1999 +0200
     2.2 +++ b/lib/Tools/makeall	Thu Aug 19 12:43:02 1999 +0200
     2.3 @@ -30,7 +30,9 @@
     2.4  
     2.5  
     2.6  SECONDS=0
     2.7 -echo -n "Started at "; date
     2.8 +DATE=$(date)
     2.9 +HOST=$(hostname)
    2.10 +echo "Started at $DATE ($HOST)"
    2.11  
    2.12  for L in $ALL_LOGICS
    2.13  do
     3.1 --- a/src/Pure/mk	Thu Aug 19 12:42:43 1999 +0200
     3.2 +++ b/src/Pure/mk	Thu Aug 19 12:43:02 1999 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4  
     3.5  if [ -z "$RAW" ]; then
     3.6    ITEM="Pure"
     3.7 -  echo -n "Building $ITEM ..."
     3.8 +  echo "Building $ITEM ..."
     3.9    LOG="$LOGDIR/$ITEM"
    3.10  
    3.11    $ISABELLE \
    3.12 @@ -90,7 +90,7 @@
    3.13    RC=$?
    3.14  else
    3.15    ITEM="RAW"
    3.16 -  echo -n "Building $ITEM ..."
    3.17 +  echo "Building $ITEM ..."
    3.18    LOG="$LOGDIR/$ITEM"
    3.19  
    3.20    $ISABELLE \
    3.21 @@ -106,10 +106,9 @@
    3.22  # exit status
    3.23  
    3.24  if [ $RC -eq 0 ]; then
    3.25 -  echo " OK  ($ELAPSED elapsed time)"
    3.26 +  echo "Finished $ITEM ($ELAPSED elapsed time)"
    3.27    gzip --force "$LOG"
    3.28  else
    3.29 -  echo
    3.30    echo "$ITEM FAILED"
    3.31    echo "(see also $LOG)"
    3.32    echo; tail $LOG; echo