diff -r bccad0374407 -r 42e13a4f52f5 lib/Tools/doc --- 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 "$@" -