--- 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