diff -r 6d0dd9491da8 -r 2a2d51f2cd95 lib/Tools/installfonts
--- a/lib/Tools/installfonts	Fri Mar 07 09:49:28 1997 +0100
+++ b/lib/Tools/installfonts	Fri Mar 07 09:56:55 1997 +0100
@@ -23,7 +23,7 @@
 
 function checkfonts()
 {
-  RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || return 1
+  RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1
 
   case "$RESULT" in
     xlsfonts:*)