author | wenzelm |
Sat, 13 Dec 2008 15:35:29 +0100 | |
changeset 29096 | 1b8e021e8c1f |
parent 29089 | 8cffa980bd93 (diff) |
parent 29095 | a75f3ed534a0 (current diff) |
child 29101 | 66fe138979f4 |
--- a/lib/Tools/usedir Sat Dec 13 15:35:18 2008 +0100 +++ b/lib/Tools/usedir Sat Dec 13 15:35:29 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 }