| author | wenzelm |
| Thu, 11 Oct 2007 15:57:29 +0200 | |
| changeset 24957 | 50959112a4e1 |
| parent 24956 | 4992239a414e |
| child 24958 | ff15f76741bd |
| lib/Tools/usedir | file | annotate | diff | comparison | revisions |
--- 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 }