etc/settings
changeset 48207 40fab092d2a2
parent 48187 6615f7ce670b
child 48443 6f2762eedca0
--- 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