changeset 7461 | 94ae093f6706 |
parent 7276 | 7a2008de228d |
child 7737 | acaf55bee03e |
--- a/lib/Tools/usedir Fri Sep 03 18:16:02 1999 +0200 +++ b/lib/Tools/usedir Fri Sep 03 18:16:54 1999 +0200 @@ -26,6 +26,8 @@ echo " Build object-logic or run examples. Also creates browsing" echo " information (HTML etc.) according to settings." echo + echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" + echo exit 1 }