changeset 2852 | ddb85eb8385f |
parent 1826 | 2a2c0dbeb4ac |
--- a/src/Tools/8bit/fonts/install Tue Apr 01 12:44:12 1997 +0200 +++ b/src/Tools/8bit/fonts/install Tue Apr 01 12:54:40 1997 +0200 @@ -1,8 +1,5 @@ #!/bin/bash -# add Isabelle 8bit fonts to X11 font path -FONTDIR=$ISABELLE8BIT/fonts +#NOTE: just a quick and dirty hack -- assumes correct isatool in PATH -# remove it first to avoid accidental double inclusion -xset fp- $FONTDIR 2>/dev/null -xset fp+ $FONTDIR +isatool installfonts