removed Cambridge font server;
authorwenzelm
Tue May 20 19:29:04 1997 +0200 (1997-05-20)
changeset 32560a45cdd7da37
parent 3255 7678f3d93053
child 3257 4e3724e0659f
removed Cambridge font server;
etc/settings
     1.1 --- a/etc/settings	Tue May 20 19:27:59 1997 +0200
     1.2 +++ b/etc/settings	Tue May 20 19:29:04 1997 +0200
     1.3 @@ -88,9 +88,9 @@
     1.4  # (1) Get fonts from local (client side) directory:
     1.5  ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
     1.6  
     1.7 -# (2) Get from font server (at Cambridge or Munich):
     1.8 +# (2) Get from font server (at Munich or Cambridge):
     1.9 +#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.10  #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
    1.11 -#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.12  
    1.13  
    1.14  ###