lib/Tools/print
author wenzelm
Sun, 13 Jun 2004 15:31:11 +0200
changeset 14936 a13d5118f628
parent 14931 7d3c1cca5341
child 15010 72fbe711e414
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14931
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     2
#
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     3
# $Id$
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     6
#
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     7
# DESCRIPTION: print document
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     8
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     9
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    11
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    12
function usage()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    13
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    14
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    15
  echo "Usage: $PRG [OPTIONS] FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    16
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    18
  echo "    -c           cleanup -- remove FILE after use"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    19
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    20
  echo "  Print document FILE."
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    21
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    22
  exit 1
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    23
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    24
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    25
function fail()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    26
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    27
  echo "$1" >&2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    28
  exit 2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    29
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    30
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    31
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    32
## process command line
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    33
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    34
# options
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    35
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    36
CLEAN=""
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    37
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    38
while getopts "c" OPT
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    39
do
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    40
  case "$OPT" in
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    41
    c)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    42
      CLEAN=true
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    43
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    44
    \?)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    45
      usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    46
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    47
  esac
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    48
done
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    49
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    50
shift $(($OPTIND - 1))
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    51
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    52
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    53
# args
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    54
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    55
[ "$#" -ne 1 ] && usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    56
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    57
FILE="$1"; shift
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    58
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    59
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    60
## main
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    61
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    62
[ -f "$FILE" ] || fail "Bad file: $FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    63
$PRINT_COMMAND "$FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    64
[ -n "$CLEAN" ] && rm -f "$FILE"