lib/fonts/README
author wenzelm
Tue, 11 Mar 1997 14:44:25 +0100
changeset 2783 7d0ec11966d4
permissions -rw-r--r--
Note on fonts and remote X11;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2783
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     1
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     2
Note on fonts and remote X11
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     3
============================
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     4
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     5
You may want to install this directory on any machine that is used as
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     6
X11 terminal for Isabelle sessions, but does not mount the full
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     7
distribution.
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     8
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
     9
In case the fonts directory does not appear on both the client and
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
    10
server side at the same location, the ISABELLE_INSTALLFONTS setting
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
    11
has to be adapted, though.
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
    12
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
    13
7d0ec11966d4 Note on fonts and remote X11;
wenzelm
parents:
diff changeset
    14
$Id$