discontinued odd XSYMBOL_INSTALLFONTS, which is private to PG-3.7.x (isafonts.informatik.tu-muenchen.de:7200 no longer exists);
authorwenzelm
Fri Jul 06 16:41:26 2012 +0200 (2012-07-06 ago)
changeset 4820740fab092d2a2
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
     1.1 --- a/etc/settings	Fri Jul 06 16:31:37 2012 +0200
     1.2 +++ b/etc/settings	Fri Jul 06 16:41:26 2012 +0200
     1.3 @@ -172,10 +172,6 @@
     1.4  PROOFGENERAL_OPTIONS=""
     1.5  #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
     1.6  
     1.7 -# Automatic setup of remote fonts
     1.8 -#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
     1.9 -XSYMBOL_INSTALLFONTS=""
    1.10 -
    1.11  
    1.12  ###
    1.13  ### Rendering information