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