# HG changeset patch
# User wenzelm
# Date 857725015 -3600
# Node ID 2a2d51f2cd955b537361e5b28e04d9995a60bd6a
# Parent  6d0dd9491da89e7a2f9c65ed64b6c42dc0e3c157
more robust check;

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:*)