src/Tools/JVM/java_ext_dirs
changeset 45385 7c1375ba1424
parent 43536 6eec653d5599
child 47113 b5a5662528fb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/java_ext_dirs	Mon Nov 07 14:59:58 2011 +0100
@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Augment Java extension directories.
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
+  isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+