src/Tools/JVM/java_ext_dirs
changeset 48915 34fac6fb9b03
parent 48914 51560e392e1b
child 48916 f45ccc0d1ace
--- 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
-