doc-src/System/Thy/document/Interfaces.tex

 
   \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed to
   the command line of any invocation of the Proof General \verb|interface| script.
 
   \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isaliteral{5F}{\isacharunderscore}}INSTALLFONTS}}}}}] may contain a small shell
-  script to install the X11 fonts required for the X-Symbols mode of
-  Proof General.  This is only relevant if the X11 display server runs
-  on a different machine than the Emacs application, with a different
-  file-system view on the Proof General installation.  Under most
-  circumstances Proof General is able to refer to the font files that
-  are part of its distribution.
+  script to install the X11 fonts required for the old X-Symbols mode
+  of Proof General.  This is only relevant if the X11 display server
+  runs on a different machine than the Emacs application, with a
+  different file-system view on the Proof General installation.  Under
+  most circumstances Proof General 3.x is able to refer to the font
+  files that are part of its distribution, and Proof General 4.x finds
+  its fonts by different means.
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %