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