diff options
author | Jean-Philippe Lesot <jplesot@google.com> | 2015-04-01 17:00:34 +0200 |
---|---|---|
committer | Jean-Philippe Lesot <jplesot@google.com> | 2015-04-01 18:07:52 +0200 |
commit | 011ec29c12763f9cc655933414b5c0a5c9a7b6ca (patch) | |
tree | cb92aea7a4539cb0c9cbc678143ca589e269f42d /jack/etc | |
parent | 98efb7bb82b1a2a3c5ada01c7b2265ecf408db82 (diff) | |
download | toolchain_jack-011ec29c12763f9cc655933414b5c0a5c9a7b6ca.tar.gz toolchain_jack-011ec29c12763f9cc655933414b5c0a5c9a7b6ca.tar.bz2 toolchain_jack-011ec29c12763f9cc655933414b5c0a5c9a7b6ca.zip |
Add local setting, add id url to Jack simple server
Change-Id: I8e4b2e51a271fe8e625c40daa13d07395981c2cf
Diffstat (limited to 'jack/etc')
-rwxr-xr-x | jack/etc/jack | 46 |
1 files changed, 38 insertions, 8 deletions
diff --git a/jack/etc/jack b/jack/etc/jack index 3a69eb62..504d935f 100755 --- a/jack/etc/jack +++ b/jack/etc/jack @@ -15,17 +15,48 @@ # limitations under the License. # set -o nounset +umask 077 # -# Default setting +# Settings # +LOCAL_SETTING="$HOME/.jack" TMPDIR=${TMPDIR:=/tmp} -SERVER_PORT=${SERVER_PORT:=8072} -SERVER_COUNT=${SERVER_COUNT:=1} -SERVER_NB_COMPILE=${SERVER_NB_COMPILE:=4} -SERVER_TIMEOUT=${SEVER_TIMEOUT:=60} -SERVER_DIR=${SERVER_DIR:=$TMPDIR/jack-$USER} -SERVER_LOG=${SERVER_LOG:=$SERVER_DIR/jack-$SERVER_PORT.log} +SERVER_DIR=$TMPDIR/jack-$USER + +# +# Create local settings if it does not exist +# +if [ ! -f "$LOCAL_SETTING" ]; then + echo "Writing local settings in " $LOCAL_SETTING + cat >"$LOCAL_SETTING.$$" <<-"EOT" + # Server settings + SERVER=true + SERVER_PORT=8072 + SERVER_COUNT=1 + SERVER_NB_COMPILE=4 + SERVER_TIMEOUT=60 + SERVER_LOG=$SERVER_DIR/jack-$SERVER_PORT.log + JACK_VM_COMMAND=${JACK_VM_COMMAND:=java} + # Internal, do not touch + SETTING_VERSION=1 +EOT + ln "$LOCAL_SETTING.$$" "$LOCAL_SETTING" + rm "$LOCAL_SETTING.$$" +fi + +# +# Load local settings +# +source "$LOCAL_SETTING" + +# +# If not in server mode, exec jack +# +if [ "$SERVER" != "true" ]; then + exec $JACK_VM_COMMAND -jar $JACK_JAR "$@" + exit 255 +fi # # Static setting @@ -42,7 +73,6 @@ JACK_CLI="$JACK_DIR/cli" JACK_EXIT="$JACK_DIR/exit" JACK_PWD="$PWD" -umask 077 mkdir "$SERVER_DIR" 2>/dev/null # Cleanup |