--- a/src/Tools/JVM/build Thu Aug 23 20:49:00 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Offline build script for JVM tools.
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## build
-
-cd "$(dirname "$0")"
-
-SOURCE="Java_Ext_Dirs.java"
-TARGET="java_ext_dirs.jar"
-
-BUILD="build_dir$$"
-TMP_JAR="java_ext_dirs$$.jar"
-
-rm -rf "$BUILD" && mkdir "$BUILD"
-javac -source 1.4 -target 1.4 -d "$BUILD" "$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"
-