equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Makarius |
|
4 # |
|
5 # DESCRIPTION: raw ML process (batch mode) |
|
6 |
|
7 isabelle_admin_build jars || exit $? |
|
8 |
|
9 case "$ISABELLE_JAVA_PLATFORM" in |
|
10 x86-*) |
|
11 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32" |
|
12 ;; |
|
13 x86_64-*) |
|
14 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64" |
|
15 ;; |
|
16 esac |
|
17 |
|
18 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
|
19 |
|
20 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? |
|
21 |
|
22 exec isabelle java isabelle.ML_Process "$@" |
|