Admin/build_polyml

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/build_polyml	Fri Nov 11 11:41:14 2016 +0100
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: build Poly/ML from sources
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+"$THIS/build" jars || exit $?
+exec "$THIS/../bin/isabelle_java" isabelle.Build_PolyML "$@"