--- a/build Thu Aug 19 12:42:43 1999 +0200
+++ b/build Thu Aug 19 12:43:02 1999 +0200
@@ -106,6 +106,7 @@
echo " ML_SYSTEM=$ML_SYSTEM"
echo " ML_HOME=$ML_HOME"
echo " ML_OPTIONS=$ML_OPTIONS"
+ echo " ML_PLATFORM=$ML_PLATFORM"
echo
echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
fi
@@ -154,7 +155,9 @@
# build it
SECONDS=0
-echo -n "Started at "; date
+DATE=$(date)
+HOST=$(hostname)
+echo "Started at $DATE ($HOST)"
export THIS_IS_ISABELLE_BUILD=true
--- a/lib/Tools/makeall Thu Aug 19 12:42:43 1999 +0200
+++ b/lib/Tools/makeall Thu Aug 19 12:43:02 1999 +0200
@@ -30,7 +30,9 @@
SECONDS=0
-echo -n "Started at "; date
+DATE=$(date)
+HOST=$(hostname)
+echo "Started at $DATE ($HOST)"
for L in $ALL_LOGICS
do
--- a/src/Pure/mk Thu Aug 19 12:42:43 1999 +0200
+++ b/src/Pure/mk Thu Aug 19 12:43:02 1999 +0200
@@ -80,7 +80,7 @@
if [ -z "$RAW" ]; then
ITEM="Pure"
- echo -n "Building $ITEM ..."
+ echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
$ISABELLE \
@@ -90,7 +90,7 @@
RC=$?
else
ITEM="RAW"
- echo -n "Building $ITEM ..."
+ echo "Building $ITEM ..."
LOG="$LOGDIR/$ITEM"
$ISABELLE \
@@ -106,10 +106,9 @@
# exit status
if [ $RC -eq 0 ]; then
- echo " OK ($ELAPSED elapsed time)"
+ echo "Finished $ITEM ($ELAPSED elapsed time)"
gzip --force "$LOG"
else
- echo
echo "$ITEM FAILED"
echo "(see also $LOG)"
echo; tail $LOG; echo