# HG changeset patch
# User berghofe
# Date 1229182173 -3600
# Node ID bebd671c6055c496e87e653e192e549d3761d7d7
# Parent  68245155eb58035c2a108ed06b947038c16a27ab# Parent  8cffa980bd93d9a59db5d979b6dc6c90b8c44bfa
merged

diff -r 68245155eb58 -r bebd671c6055 lib/Tools/usedir
--- a/lib/Tools/usedir	Sat Dec 13 13:24:45 2008 +0100
+++ b/lib/Tools/usedir	Sat Dec 13 16:29:33 2008 +0100
@@ -40,6 +40,11 @@
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
+  echo "  ML_PLATFORM=$ML_PLATFORM"
+  echo "  ML_HOME=$ML_HOME"
+  echo "  ML_SYSTEM=$ML_SYSTEM"
+  echo "  ML_OPTIONS=$ML_OPTIONS"
+  echo
   exit 1
 }