diff -r dffa657f0aa2 -r 7c1375ba1424 lib/scripts/java_ext_dirs
--- a/lib/scripts/java_ext_dirs	Mon Nov 07 14:23:50 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Augment Java extension directories.
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## dependencies
-
-SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
-
-TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/java_ext_dirs.jar"
-
-if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
-  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
-  pushd "$TARGET_DIR" >/dev/null
-
-  BUILD="build$$"
-  TMP_JAR="java_ext_dirs$$.jar"
-
-  rm -rf "$BUILD" && mkdir "$BUILD"
-  javac -d "$BUILD" -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
-  jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce $TMP_JAR"
-  mv "$TMP_JAR" "$TARGET"
-  rm -rf "$BUILD"
-
-  popd >/dev/null
-fi
-
-
-## main
-
-JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
-  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
-