--- 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")"
-