# HG changeset patch
# User wenzelm
# Date 935161051 -7200
# Node ID 1ef2c659023d63310939f1fed7fde31d1a9c365d
# Parent  298b0dcadf2ef9e5646b7c984145344b7f9f9833
echo ML_PLATFORM;

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