lib/Tools/installfonts
author wenzelm
Tue Feb 04 08:59:17 1997 +0100 (1997-02-04)
changeset 2578 cc768a16ef65
parent 2335 e965156e84e3
child 2746 2a2d51f2cd95
permissions -rwxr-xr-x
now uses ISABELLE_INSTALLFONTS;
     1 #!/bin/bash -norc
     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 ## check for isabelle fonts
    23 
    24 function checkfonts()
    25 {
    26   RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || return 1
    27 
    28   case "$RESULT" in
    29     xlsfonts:*)
    30       return 1
    31       ;;
    32   esac
    33 
    34   return 0
    35 }
    36 
    37 
    38 ## main
    39 
    40 [ $# -ne 0 ] && usage
    41 
    42 checkfonts || eval $ISABELLE_INSTALLFONTS
    43 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2