diff -r 355b78441650 -r 1e23caac8757 Admin/build_history
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/build_history	Mon Oct 03 16:50:29 2016 +0200
@@ -0,0 +1,10 @@
+#!/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 "$@"