runServer.sh 741 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
#!/bin/sh

# set default lib path
if [ -z "${DISL_LIB_P}" ]; then
	DISL_LIB_P=./build
fi

# available options
#    -Ddebug=true \
#    -Ddisl.classes="list of disl classes (: - separator)"
#    -Ddisl.noexcepthandler=true \
#    -Ddisl.exclusionList="path" \
#    -Ddislserver.instrumented="path" \
#    -Ddislserver.uninstrumented="path" \
#    -Ddislserver.port="portNum" \
#    -Ddislserver.timestat=true \
#    -Ddislserver.continuous=true \

# get instrumentation library and shift parameters
INSTR_LIB=$1
shift

# start server
java $* \
     -cp ${INSTR_LIB}:${DISL_LIB_P}/disl-server.jar \
     ch.usi.dag.dislserver.DiSLServer \
     &

# print pid to the server file
if [ -n "${SERVER_FILE}" ]; then
    echo $! > ${SERVER_FILE}
fi