diff -r 51560e392e1b -r 34fac6fb9b03 src/Tools/JVM/java_ext_dirs --- a/src/Tools/JVM/java_ext_dirs Thu Aug 23 20:49:00 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -#!/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 - -isabelle_jdk java -Dfile.encoding=UTF-8 \ - -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \ - isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null -