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