| author | kleing |
| Tue, 29 Jun 2004 11:18:34 +0200 | |
| changeset 15010 | 72fbe711e414 |
| parent 14997 | aa2aaab41566 |
| child 15218 | 39747a9e3c37 |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # $Id$
4 # Author: Markus Wenzel, TU Muenchen
5 #
6 # DESCRIPTION: display document (in DVI format)
9 PRG="$(basename "$0")"
11 function usage()
12 {
13 echo
14 echo "Usage: $PRG [OPTIONS] FILE"
15 echo
16 echo " Options are:"
17 echo " -c cleanup -- remove FILE after use"
18 echo
19 echo " Display document FILE (in DVI format)."
20 echo
21 exit 1
22 }
24 function fail()
25 {
26 echo "$1" >&2
27 exit 2
28 }
31 ## process command line
33 # options
35 CLEAN=""
37 while getopts "c" OPT
38 do
39 case "$OPT" in
40 c)
41 CLEAN=true
42 ;;
43 \?)
44 usage
45 ;;
46 esac
47 done
49 shift $(($OPTIND - 1))
52 # args
54 [ "$#" -ne 1 ] && usage
56 FILE="$1"; shift
59 ## main
61 [ -f "$FILE" ] || fail "Bad file: $FILE"
63 if [ -n "$CLEAN" ]; then
64 PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi
65 mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
66 $DVI_VIEWER "$PRIVATE_FILE"
67 rm -f "$PRIVATE_FILE"
68 else
69 exec $DVI_VIEWER "$FILE"
70 fi