lib/Tools/doc
changeset 62438 42e13a4f52f5
parent 52444 2cfe6656d6d6
child 62589 b5783412bfed
--- a/lib/Tools/doc	Sat Feb 27 19:47:53 2016 +0100
+++ b/lib/Tools/doc	Sat Feb 27 19:57:36 2016 +0100
@@ -4,34 +4,6 @@
 #
 # DESCRIPTION: view Isabelle documentation
 
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [DOC ...]"
-  echo
-  echo "  View Isabelle documentation."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## args
-
-[ "$#" -eq 1 -a "$1" = "-?" ] && usage
-
-
-## main
-
 isabelle_admin_build jars || exit $?
 
 "$ISABELLE_TOOL" java isabelle.Doc "$@"
-