lib/Tools/installfonts
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 3253 ea75747190a7
child 9974 5361a27c1853
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: install the isabelle fonts into your X11 server
     8 
     9 
    10 PRG=$(basename "$0")
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG"
    16   echo
    17   echo "  Install the isabelle fonts into your X11 server."
    18   echo "  (May be safely called repeatedly.)"
    19   echo
    20   exit 1
    21 }
    22 
    23 
    24 ## check for isabelle fonts
    25 
    26 function checkfonts()
    27 {
    28   RESULT=$(xlsfonts -fn "-isabelle-fixed-*-isabelle-0" 2>&1) || return 1
    29 
    30   case "$RESULT" in
    31     xlsfonts:*)
    32       return 1
    33       ;;
    34   esac
    35 
    36   return 0
    37 }
    38 
    39 
    40 ## main
    41 
    42 [ "$#" -ne 0 ] && usage
    43 
    44 checkfonts || eval $ISABELLE_INSTALLFONTS
    45 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2