changeset 3312 | 6ec687d436aa |
parent 3303 | 656b5221a56e |
child 3349 | 943d1630f003 |
--- a/etc/settings Fri May 23 10:14:16 1997 +0200 +++ b/etc/settings Fri May 23 11:28:22 1997 +0200 @@ -88,9 +88,8 @@ # (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 Munich or Cambridge): +# (2) Get from font server at Munich: #ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" -#ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" ###