author | berghofe |
Sat, 13 Dec 2008 16:29:33 +0100 | |
changeset 29099 | bebd671c6055 |
parent 29097 | 68245155eb58 (current diff) |
parent 29089 | 8cffa980bd93 (diff) |
child 29100 | 933145f5a9ba |
--- 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 }