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