# HG changeset patch
# User wenzelm
# Date 1192121914 -7200
# Node ID 592a5d8700a7e2988947343fad3e79e98c3fbf4c
# Parent  a2f15968a6f2a2069d0623525dea6f6427508bff
usedir: added HOL_USEDIR_OPTIONS;

diff -r a2f15968a6f2 -r 592a5d8700a7 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}