diff -r 802576856527 -r 09e52d4a850a lib/Tools/print
--- a/lib/Tools/print	Sun Jul 07 18:34:29 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: print document
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] FILE"
-  echo
-  echo "  Options are:"
-  echo "    -c           cleanup -- remove FILE after use"
-  echo
-  echo "  Print document FILE."
-  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"
-$PRINT_COMMAND "$FILE"
-[ -n "$CLEAN" ] && rm -f "$FILE"