lib/Tools/usedir

--- a/lib/Tools/usedir	Thu Oct 11 10:23:09 2007 +0200
+++ b/lib/Tools/usedir	Thu Oct 11 15:57:29 2007 +0200
@@ -38,6 +38,7 @@
   echo "  information (HTML etc.) according to settings."
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
+  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
   exit 1
 }