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