echo ML_PLATFORM;
authorwenzelm
Fri Aug 20 16:57:31 1999 +0200 (1999-08-20 ago)
changeset 73111ef2c659023d
parent 7310 298b0dcadf2e
child 7312 523fb2832b30
echo ML_PLATFORM;
build
     1.1 --- a/build	Fri Aug 20 16:16:16 1999 +0200
     1.2 +++ b/build	Fri Aug 20 16:57:31 1999 +0200
     1.3 @@ -146,6 +146,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    echo