# HG changeset patch
# User wenzelm
# Date 1341585686 -7200
# Node ID 40fab092d2a2019a27208310e37c6250260749f9
# Parent  937b53a339f065c0db6e9daefc9fe3c177c2a69d
discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);

diff -r 937b53a339f0 -r 40fab092d2a2 etc/settings
--- a/etc/settings	Fri Jul 06 16:31:37 2012 +0200
+++ b/etc/settings	Fri Jul 06 16:41:26 2012 +0200
@@ -172,10 +172,6 @@
 PROOFGENERAL_OPTIONS=""
 #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
 
-# Automatic setup of remote fonts
-#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
-XSYMBOL_INSTALLFONTS=""
-
 
 ###
 ### Rendering information