usage: tell OPTIONS;

--- a/doc-src/System/misc.tex	Fri Sep 03 18:17:51 1999 +0200
+++ b/doc-src/System/misc.tex	Fri Sep 03 18:30:14 1999 +0200
@@ -228,6 +228,8 @@
 
   Build object-logic or run examples. Also creates browsing
   information (HTML etc.) according to settings.
+
+  ISABELLE_USEDIR_OPTIONS=
 \end{ttbox}
 
 Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is