| changeset 29089 | 8cffa980bd93 |
| parent 28650 | a7ba12e0d3b7 |
| child 29143 | 72c960b2b83e |
--- 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 }