--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/display Sun Jun 13 15:28:12 2004 +0200
@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# DESCRIPTION: display document (in DVI format)
+
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] FILE"
+ echo
+ echo " Options are:"
+ echo " -c cleanup -- remove FILE after use"
+ echo
+ echo " Display document FILE (in DVI format)."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+CLEAN=""
+
+while getopts "c" OPT
+do
+ case "$OPT" in
+ c)
+ CLEAN=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+FILE="$1"; shift
+
+
+## main
+
+[ -f "$FILE" ] || fail "Bad file: $FILE"
+
+if [ -n "$CLEAN" ]; then
+ PRIVATE_FILE=$(basename "$FILE" .dvi)$$.dvi
+ mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
+ $DVI_VIEWER "$PRIVATE_FILE"
+ rm -f "$PRIVATE_FILE"
+else
+ exec $DVI_VIEWER "$FILE"
+fi