+−#!/usr/bin/env bash +−# +−# DESCRIPTION: build history versions from another repository clone +− +−unset CDPATH +−THIS="$(cd "$(dirname "$0")"; pwd)" +− +−"$THIS/../bin/isabelle" scala_build -q || exit $? +−"$THIS/../bin/isabelle_java" isabelle.Build_History "$@"