| changeset 53441 | 63958e9e0073 |
| parent 53440 | b99d006afbfe |
| child 53445 | 811db2b751ed |
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 06 17:20:48 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 06 17:26:58 2013 +0200 @@ -171,7 +171,6 @@ } declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)" -[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"