discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);
authorwenzelm
Fri, 06 Jul 2012 16:41:26 +0200
changeset 48207 40fab092d2a2
parent 48206 937b53a339f0
child 48208 bde354773a56
discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);
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