doc-src/System/fonts.tex
changeset 7849 29a2a1d71128
parent 5364 ffa6d795c4b3
child 7882 52fb3667f7df
--- a/doc-src/System/fonts.tex	Wed Oct 13 15:41:24 1999 +0200
+++ b/doc-src/System/fonts.tex	Wed Oct 13 19:39:19 1999 +0200
@@ -52,8 +52,7 @@
 same machine. In this 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"
-
+ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$
 \end{ttbox}
 The same also works for remote X11 sessions in a somewhat homogeneous
 network, where any X11 display machine also mounts the Isabelle
@@ -134,7 +133,6 @@
 scripts are just left in plain \textsc{ascii}.  Thus users with
 \textsc{ascii}-only facilities will still be able to read your files.
 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "system"