build
changeset 7277 bb9502f9154a
parent 6256 e17fb80b3ce1
child 7311 1ef2c659023d
--- 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