# HG changeset patch
# User wenzelm
# Date 1087133292 -7200
# Node ID 24a0b2dd9be697ecfd1c7cbddc803eb7dcdce024
# Parent  7f1ff621085ef547a25c9c94c025b5e02e36fe95
display document (in DVI format)

diff -r 7f1ff621085e -r 24a0b2dd9be6 lib/Tools/display
--- /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