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