usedir: added HOL_USEDIR_OPTIONS;
authorwenzelm
Thu, 11 Oct 2007 18:58:34 +0200
changeset 24975 592a5d8700a7
parent 24974 a2f15968a6f2
child 24976 821628d16552
usedir: added HOL_USEDIR_OPTIONS;
doc-src/System/present.tex
--- a/doc-src/System/present.tex	Thu Oct 11 16:51:39 2007 +0200
+++ b/doc-src/System/present.tex	Thu Oct 11 18:58:34 2007 +0200
@@ -381,6 +381,7 @@
   information (HTML etc.) according to settings.
 
   ISABELLE_USEDIR_OPTIONS=
+  HOL_USEDIR_OPTIONS=
 \end{ttbox}
 
 Note that the value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is
@@ -390,6 +391,10 @@
 globally via above variable. In particular, generation of \rmindex{HTML}
 browsing information and document preparation is controlled here.
 
+The \settdx{HOL_USEDIR_OPTIONS} setting is specific to the main
+Isabelle/HOL image; its value is appended to
+\verb,ISABELLE_USEDIR_OPTIONS, for that particular session only.
+
 
 \subsection*{Options}