tuned comment;
authorwenzelm
Tue, 11 Mar 1997 16:17:01 +0100
changeset 2784a78655c814b0
parent 2783 7d0ec11966d4
child 2785 27a17c846021
tuned comment;
more robust check;
lib/Tools/installfonts
     1.1 --- a/lib/Tools/installfonts	Tue Mar 11 14:44:25 1997 +0100
     1.2 +++ b/lib/Tools/installfonts	Tue Mar 11 16:17:01 1997 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  #
     1.5  # $Id$
     1.6  #
     1.7 -# DESCRIPTION: install Isabelle symbol fonts
     1.8 +# DESCRIPTION: install the isabelle fonts into your X11 server
     1.9  
    1.10  
    1.11  PRG=$(basename $0)
    1.12 @@ -12,7 +12,7 @@
    1.13    echo
    1.14    echo "Usage: $PRG"
    1.15    echo
    1.16 -  echo "  Install the Isabelle symbol fonts into your X11 server."
    1.17 +  echo "  Install the isabelle fonts into your X11 server."
    1.18    echo "  (May be savely called repeatedly.)"
    1.19    echo
    1.20    exit 1
    1.21 @@ -23,7 +23,7 @@
    1.22  
    1.23  function checkfonts()
    1.24  {
    1.25 -  RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1
    1.26 +  RESULT=$(xlsfonts -fn "-isabelle-fixed-*-isabelle-0" 2>&1) || return 1
    1.27  
    1.28    case "$RESULT" in
    1.29      xlsfonts:*)