diff -r 7678f3d93053 -r 0a45cdd7da37 etc/settings --- a/etc/settings Tue May 20 19:27:59 1997 +0200 +++ b/etc/settings Tue May 20 19:29:04 1997 +0200 @@ -88,9 +88,9 @@ # (1) Get fonts from local (client side) directory: ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" -# (2) Get from font server (at Cambridge or Munich): +# (2) Get from font server (at Munich or Cambridge): +#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" -#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" ###