wenzelm@64021: #!/usr/bin/env bash
wenzelm@64021: #
wenzelm@64021: # DESCRIPTION: build history versions from another repository clone
wenzelm@64021: 
wenzelm@64021: THIS="$(cd "$(dirname "$0")"; pwd)"
wenzelm@64021: 
wenzelm@64223: "$THIS/build" jars > /dev/null || exit $?
wenzelm@64021: exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"