equal
deleted
inserted
replaced
77 } |
77 } |
78 |
78 |
79 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)" |
79 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)" |
80 [ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" |
80 [ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" |
81 |
81 |
|
82 "$ISABELLE_TOOL" java -server >/dev/null 2>/dev/null && \ |
|
83 JAVA_ARGS["${#JAVA_ARGS[@]}"]="-server" |
|
84 |
82 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)" |
85 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)" |
83 |
86 |
84 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
87 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
85 getoptions "${OPTIONS[@]}" |
88 getoptions "${OPTIONS[@]}" |
86 |
89 |