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;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2297
     2
#
wenzelm@2311
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2311
     6
#
wenzelm@2784
     7
# DESCRIPTION: install the isabelle fonts into your X11 server
wenzelm@2311
     8
wenzelm@2297
     9
wenzelm@9788
    10
PRG=$(basename "$0")
wenzelm@2297
    11
wenzelm@2297
    12
function usage()
wenzelm@2297
    13
{
wenzelm@2297
    14
  echo
wenzelm@2297
    15
  echo "Usage: $PRG"
wenzelm@2297
    16
  echo
wenzelm@2784
    17
  echo "  Install the isabelle fonts into your X11 server."
wenzelm@3253
    18
  echo "  (May be safely called repeatedly.)"
wenzelm@2297
    19
  echo
wenzelm@2297
    20
  exit 1
wenzelm@2297
    21
}
wenzelm@2297
    22
wenzelm@2297
    23
wenzelm@2578
    24
## check for isabelle fonts
wenzelm@2578
    25
wenzelm@2578
    26
function checkfonts()
wenzelm@2578
    27
{
wenzelm@2784
    28
  RESULT=$(xlsfonts -fn "-isabelle-fixed-*-isabelle-0" 2>&1) || return 1
wenzelm@2578
    29
wenzelm@2578
    30
  case "$RESULT" in
wenzelm@2578
    31
    xlsfonts:*)
wenzelm@2578
    32
      return 1
wenzelm@2578
    33
      ;;
wenzelm@2578
    34
  esac
wenzelm@2578
    35
wenzelm@2578
    36
  return 0
wenzelm@2578
    37
}
wenzelm@2578
    38
wenzelm@2578
    39
wenzelm@2297
    40
## main
wenzelm@2297
    41
wenzelm@9788
    42
[ "$#" -ne 0 ] && usage
wenzelm@2297
    43
wenzelm@2578
    44
checkfonts || eval $ISABELLE_INSTALLFONTS
wenzelm@2578
    45
checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2