Admin/build_history
author wenzelm
Wed, 12 Oct 2016 11:48:53 +0200
changeset 64165 2e1b25d6c108
parent 64021 1e23caac8757
child 64200 2e6597279d38
permissions -rwxr-xr-x
modernized;

#!/usr/bin/env bash
#
# DESCRIPTION: build history versions from another repository clone


THIS="$(cd "$(dirname "$0")"; pwd)"

"$THIS/build" jars || exit $?

exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"