lib/Tools/installfonts
changeset 2784 a78655c814b0
parent 2746 2a2d51f2cd95
child 3007 e5efa177ee0c
equal deleted inserted replaced
2783:7d0ec11966d4 2784:a78655c814b0
     1 #!/bin/bash -norc
     1 #!/bin/bash -norc
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: install Isabelle symbol fonts
     5 # DESCRIPTION: install the isabelle fonts into your X11 server
     6 
     6 
     7 
     7 
     8 PRG=$(basename $0)
     8 PRG=$(basename $0)
     9 
     9 
    10 function usage()
    10 function usage()
    11 {
    11 {
    12   echo
    12   echo
    13   echo "Usage: $PRG"
    13   echo "Usage: $PRG"
    14   echo
    14   echo
    15   echo "  Install the Isabelle symbol fonts into your X11 server."
    15   echo "  Install the isabelle fonts into your X11 server."
    16   echo "  (May be savely called repeatedly.)"
    16   echo "  (May be savely called repeatedly.)"
    17   echo
    17   echo
    18   exit 1
    18   exit 1
    19 }
    19 }
    20 
    20 
    21 
    21 
    22 ## check for isabelle fonts
    22 ## check for isabelle fonts
    23 
    23 
    24 function checkfonts()
    24 function checkfonts()
    25 {
    25 {
    26   RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1
    26   RESULT=$(xlsfonts -fn "-isabelle-fixed-*-isabelle-0" 2>&1) || return 1
    27 
    27 
    28   case "$RESULT" in
    28   case "$RESULT" in
    29     xlsfonts:*)
    29     xlsfonts:*)
    30       return 1
    30       return 1
    31       ;;
    31       ;;