remove cl.cam font server;
authorwenzelm
Fri, 23 May 1997 11:28:22 +0200
changeset 3312 6ec687d436aa
parent 3311 36e3de24137d
child 3313 b00902bb16ca
remove cl.cam font server;
etc/settings
--- 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"
 
 
 ###