--- a/lib/Tools/display Sat Sep 26 11:43:25 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: display document (in DVI or PDF format)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG DOCUMENT"
- echo
- echo " Display DOCUMENT (in DVI or PDF format)."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-[ "$#" -ne 1 -o "$1" = "-?" ] && usage
-
-DOCUMENT="$1"; shift
-
-[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
-
-case "$DOCUMENT" in
- *.dvi)
- exec "$DVI_VIEWER" "$DOCUMENT"
- ;;
- *.pdf)
- exec "$PDF_VIEWER" "$DOCUMENT"
- ;;
- *)
- fail "Unknown document type: \"$DOCUMENT\"";
-esac
-