src/Tools/JVM/build

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/JVM/build	Mon Nov 07 14:59:58 2011 +0100
@@ -0,0 +1,31 @@
+#!/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"
+