lib/fontserver/config-sample
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 9818 71de955e8fc9
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3251
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     1
#
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     2
# $Id$
9818
wenzelm
parents: 3291
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 3291
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
3251
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     5
#
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     6
# X11 font server sample configuration
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     7
# (Cf. your local man page of 'xfs' or 'fs'!)
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     8
#
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
     9
#
3284
b7f0c0af4071 tuned comments;
wenzelm
parents: 3251
diff changeset
    10
# Edit a copy of this file and run your server like this:
3251
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    11
#
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    12
#   xfs -config /foo/bar/fontserver/config
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    13
#
3291
wenzelm
parents: 3284
diff changeset
    14
#
wenzelm
parents: 3284
diff changeset
    15
# Then test it by any of the these commands (replace foo by your
wenzelm
parents: 3284
diff changeset
    16
# host name):
3251
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    17
#
3291
wenzelm
parents: 3284
diff changeset
    18
#   fsinfo -server foo:7200
wenzelm
parents: 3284
diff changeset
    19
#   fslsfonts -server foo:7200
wenzelm
parents: 3284
diff changeset
    20
#   xset fp+ tcp/foo:7200
3251
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    21
#
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    22
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    23
# the standard port is 7100, this might be already in use
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    24
#port = 7100
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    25
port = 7200
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    26
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    27
# location of the Isabelle font files
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    28
catalogue = /usr/proj/isabelle/lib/fonts
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    29
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    30
# number of client sessions we accept
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    31
client-limit = 50
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    32
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    33
# where to put error messages
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    34
use-syslog = on
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    35
#use-syslog = off
0b74b9d4439e X11 font server sample configuration;
wenzelm
parents:
diff changeset
    36
#error-file = /var/tmp/fontserver-errors