# HG changeset patch
# User wenzelm
# Date 858093421 -3600
# Node ID a78655c814b0ef83488c84ce25412ad1aec256e4
# Parent  7d0ec11966d48674590fe52185aadd3bdaf24086
tuned comment;
more robust check;

diff -r 7d0ec11966d4 -r a78655c814b0 lib/Tools/installfonts
--- a/lib/Tools/installfonts	Tue Mar 11 14:44:25 1997 +0100
+++ b/lib/Tools/installfonts	Tue Mar 11 16:17:01 1997 +0100
@@ -2,7 +2,7 @@
 #
 # $Id$
 #
-# DESCRIPTION: install Isabelle symbol fonts
+# DESCRIPTION: install the isabelle fonts into your X11 server
 
 
 PRG=$(basename $0)
@@ -12,7 +12,7 @@
   echo
   echo "Usage: $PRG"
   echo
-  echo "  Install the Isabelle symbol fonts into your X11 server."
+  echo "  Install the isabelle fonts into your X11 server."
   echo "  (May be savely called repeatedly.)"
   echo
   exit 1
@@ -23,7 +23,7 @@
 
 function checkfonts()
 {
-  RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1
+  RESULT=$(xlsfonts -fn "-isabelle-fixed-*-isabelle-0" 2>&1) || return 1
 
   case "$RESULT" in
     xlsfonts:*)