lib/Tools/print
author wenzelm
Thu, 19 Jan 2006 21:22:15 +0100
changeset 18710 527aa560a9e0
parent 15010 72fbe711e414
child 28650 a7ba12e0d3b7
permissions -rwxr-xr-x
tuned comments;
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
#
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     6
# DESCRIPTION: print document
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     7
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     8
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
     9
PRG="$(basename "$0")"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    10
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    11
function usage()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    12
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    13
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    14
  echo "Usage: $PRG [OPTIONS] FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    15
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    16
  echo "  Options are:"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    17
  echo "    -c           cleanup -- remove FILE after use"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    18
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    19
  echo "  Print document FILE."
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    20
  echo
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    21
  exit 1
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    22
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    23
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    24
function fail()
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    25
{
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    27
  exit 2
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    28
}
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    29
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    30
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    31
## process command line
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    32
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    33
# options
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    34
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    35
CLEAN=""
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    36
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    37
while getopts "c" OPT
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    38
do
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    39
  case "$OPT" in
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    40
    c)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    41
      CLEAN=true
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    42
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    43
    \?)
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    44
      usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    45
      ;;
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    46
  esac
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    47
done
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    48
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    49
shift $(($OPTIND - 1))
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    50
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    51
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    52
# args
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    53
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    54
[ "$#" -ne 1 ] && usage
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    55
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    56
FILE="$1"; shift
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    57
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    58
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    59
## main
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    60
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    61
[ -f "$FILE" ] || fail "Bad file: $FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    62
$PRINT_COMMAND "$FILE"
7d3c1cca5341 print document
wenzelm
parents:
diff changeset
    63
[ -n "$CLEAN" ] && rm -f "$FILE"