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;
wenzelm@2297
     1
#!/bin/bash
wenzelm@2297
     2
#
wenzelm@2311
     3
# $Id$
wenzelm@2311
     4
#
wenzelm@2297
     5
# DESCRIPTION: install Isabelle symbol fonts
wenzelm@2311
     6
wenzelm@2297
     7
wenzelm@2297
     8
PRG=$(basename $0)
wenzelm@2297
     9
wenzelm@2297
    10
function usage()
wenzelm@2297
    11
{
wenzelm@2297
    12
  echo
wenzelm@2297
    13
  echo "Usage: $PRG"
wenzelm@2297
    14
  echo
wenzelm@2297
    15
  echo "  Install the Isabelle symbol fonts into your X11 server."
wenzelm@2297
    16
  echo "  (May be savely called repeatedly.)"
wenzelm@2297
    17
  echo
wenzelm@2297
    18
  exit 1
wenzelm@2297
    19
}
wenzelm@2297
    20
wenzelm@2297
    21
wenzelm@2297
    22
## main
wenzelm@2297
    23
wenzelm@2297
    24
[ $# -ne 0 ] && usage
wenzelm@2297
    25
wenzelm@2297
    26
wenzelm@2311
    27
RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || exit 1
wenzelm@2297
    28
wenzelm@2297
    29
case "$RESULT" in
wenzelm@2297
    30
  xlsfonts:*)
wenzelm@2297
    31
    xset fp+ $ISABELLE_HOME/lib/fonts
wenzelm@2297
    32
    xset fp rehash
wenzelm@2297
    33
    ;;
wenzelm@2297
    34
esac