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