# HG changeset patch
# User wenzelm
# Date 1229178793 -3600
# Node ID 8cffa980bd93d9a59db5d979b6dc6c90b8c44bfa
# Parent  95a239a5e0558ef6a17cc596dfeb32b60484d8d8
usage: echo ML settings as well;

diff -r 95a239a5e055 -r 8cffa980bd93 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Dec 12 12:14:02 2008 +0100
+++ b/lib/Tools/usedir	Sat Dec 13 15:33:13 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
 }