discontinued XSYMBOL_INSTALLFONTS (cf. 40fab092d2a2);

--- a/doc-src/System/Thy/Interfaces.thy	Fri Jul 06 16:41:26 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy	Sat Jul 07 19:36:50 2012 +0200
@@ -61,15 +61,6 @@
   the command line of any invocation of the Proof General @{verbatim
   interface} script.
 
-  \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
-  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}
 *}
 

--- a/doc-src/System/Thy/document/Interfaces.tex	Fri Jul 06 16:41:26 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex	Sat Jul 07 19:36:50 2012 +0200
@@ -81,15 +81,6 @@
   \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 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%