diff -r 298b0dcadf2e -r 1ef2c659023d build
--- a/build	Fri Aug 20 16:16:16 1999 +0200
+++ b/build	Fri Aug 20 16:57:31 1999 +0200
@@ -146,6 +146,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"
   echo