lib/Tools/installfonts
author wenzelm
Tue Apr 22 11:37:12 1997 +0200 (1997-04-22)
changeset 3007 e5efa177ee0c
parent 2784 a78655c814b0
child 3253 ea75747190a7
permissions -rwxr-xr-x
removed -norc;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: install the isabelle fonts into your X11 server
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG"
    14   echo
    15   echo "  Install the isabelle 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-fixed-*-isabelle-0" 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