lib/Tools/installfonts
author wenzelm
Fri, 07 Mar 1997 09:56:55 +0100
changeset 2746 2a2d51f2cd95
parent 2578 cc768a16ef65
child 2784 a78655c814b0
permissions -rwxr-xr-x
more robust check;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2335
e965156e84e3 added -norc option;
wenzelm
parents: 2311
diff changeset
     1
#!/bin/bash -norc
2297
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
2578
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    22
## check for isabelle fonts
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    23
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    24
function checkfonts()
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    25
{
2746
2a2d51f2cd95 more robust check;
wenzelm
parents: 2578
diff changeset
    26
  RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1
2578
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    27
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    28
  case "$RESULT" in
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    29
    xlsfonts:*)
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    30
      return 1
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    31
      ;;
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    32
  esac
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    33
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    34
  return 0
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    35
}
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    36
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    37
2297
efcabc6df91a installfonts: install Isabelle symbol fonts.
wenzelm
parents:
diff changeset
    38
## main
efcabc6df91a installfonts: install Isabelle symbol fonts.
wenzelm
parents:
diff changeset
    39
efcabc6df91a installfonts: install Isabelle symbol fonts.
wenzelm
parents:
diff changeset
    40
[ $# -ne 0 ] && usage
efcabc6df91a installfonts: install Isabelle symbol fonts.
wenzelm
parents:
diff changeset
    41
2578
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    42
checkfonts || eval $ISABELLE_INSTALLFONTS
cc768a16ef65 now uses ISABELLE_INSTALLFONTS;
wenzelm
parents: 2335
diff changeset
    43
checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2