author wenzelm
Tue, 11 Mar 1997 14:44:25 +0100
changeset 2783 7d0ec11966d4
permissions -rw-r--r--
Note on fonts and remote X11;

Note on fonts and remote X11

You may want to install this directory on any machine that is used as
X11 terminal for Isabelle sessions, but does not mount the full

In case the fonts directory does not appear on both the client and
server side at the same location, the ISABELLE_INSTALLFONTS setting
has to be adapted, though.