lib/Tools/installfonts
author wenzelm
Wed Dec 04 13:10:52 1996 +0100 (1996-12-04)
changeset 2311 69c51db9481f
parent 2297 efcabc6df91a
child 2335 e965156e84e3
permissions -rwxr-xr-x
fails more gracefully;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: install Isabelle symbol fonts
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG"
    14   echo
    15   echo "  Install the Isabelle symbol fonts into your X11 server."
    16   echo "  (May be savely called repeatedly.)"
    17   echo
    18   exit 1
    19 }
    20 
    21 
    22 ## main
    23 
    24 [ $# -ne 0 ] && usage
    25 
    26 
    27 RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || exit 1
    28 
    29 case "$RESULT" in
    30   xlsfonts:*)
    31     xset fp+ $ISABELLE_HOME/lib/fonts
    32     xset fp rehash
    33     ;;
    34 esac