diff -r dffa657f0aa2 -r 7c1375ba1424 src/Tools/JVM/java_ext_dirs --- /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")" +