# HG changeset patch
# User wenzelm
# Date 1001678654 -7200
# Node ID ee1247ba494124f29078bd4ccfaaef13efe73fe3
# Parent  ca7be12b2cbcc19952eb7dce82a4baddf7dfe30d
tuned;

diff -r ca7be12b2cbc -r ee1247ba4941 doc-src/System/fonts.tex
--- a/doc-src/System/fonts.tex	Fri Sep 28 11:08:53 2001 +0200
+++ b/doc-src/System/fonts.tex	Fri Sep 28 14:04:14 2001 +0200
@@ -58,8 +58,8 @@
 case, most X11 display servers should be happy by being told about the
 Isabelle fonts directory as follows:
 \begin{ttbox}
-ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$
-\end{ttbox}
+ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
+\end{ttbox}%$
 The same also works for remote X11 sessions in a largely homogeneous network,
 where any X11 display machine also mounts the Isabelle distribution under the
 \emph{same} name as the client side.
diff -r ca7be12b2cbc -r ee1247ba4941 doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Fri Sep 28 11:08:53 2001 +0200
+++ b/doc-src/System/misc.tex	Fri Sep 28 14:04:14 2001 +0200
@@ -187,6 +187,7 @@
 
 
 \section{Isabelle's version of make --- \texttt{isatool make}}
+\label{sec:tool-make}
 
 The Isabelle \tooldx{make} utility is a very simple wrapper for
 ordinary Unix \texttt{make}:
diff -r ca7be12b2cbc -r ee1247ba4941 doc-src/System/present.tex
--- a/doc-src/System/present.tex	Fri Sep 28 11:08:53 2001 +0200
+++ b/doc-src/System/present.tex	Fri Sep 28 14:04:14 2001 +0200
@@ -11,9 +11,13 @@
 and \texttt{HOL} from \texttt{Pure}), and application sessions in leaf
 positions.  The latter usually do not have a separate {\ML} image.
 
-The \texttt{usedir} and \texttt{mkdir} utilities provide the prime means for
-managing Isabelle sessions, including proper setup for presentation (see
-\S\ref{sec:tool-usedir} and \S\ref{sec:tool-mkdir}).
+The \texttt{mkdir} (see \S\ref{sec:tool-mkdir}) and \texttt{make} (see
+\S\ref{sec:tool-make}) tools of Isabelle provide the primary means for
+managing Isabelle sessions, including proper setup for presentation.  Here the
+\texttt{usedir} (see \S\ref{sec:tool-usedir}) tool takes care to run any
+additional stages required for document preparation, notably the tools
+\texttt{document} (see \S\ref{sec:tool-document}) and \texttt{latex} (see
+\S\ref{sec:tool-latex}).
 
 
 \section{Generating theory browsing information} \label{sec:info}