src/Tools/8bit/fonts/install
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