src/Tools/JVM/build
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45385 7c1375ba1424
permissions -rwxr-xr-x
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45385
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     2
#
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     4
#
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     5
# Offline build script for JVM tools.
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     6
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     7
## diagnostics
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     8
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
     9
function fail()
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    10
{
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    11
  echo "$1" >&2
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    12
  exit 2
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    13
}
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    14
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    15
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    16
## build
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    17
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    18
cd "$(dirname "$0")"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    19
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    20
SOURCE="Java_Ext_Dirs.java"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    21
TARGET="java_ext_dirs.jar"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    22
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    23
BUILD="build_dir$$"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    24
TMP_JAR="java_ext_dirs$$.jar"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    25
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    26
rm -rf "$BUILD" && mkdir "$BUILD"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    27
javac -source 1.4 -target 1.4 -d "$BUILD" "$SOURCE" || fail "Failed to compile sources"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    28
jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce \"$TMP_JAR\""
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    29
mv "$TMP_JAR" "$TARGET"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    30
rm -rf "$BUILD"
7c1375ba1424 offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
diff changeset
    31