| changeset 34843 | eb8806a2e348 |
| parent 34790 | 643c48774b17 |
| child 34880 | f88fc4fcab86 |
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Fri Jan 08 12:25:37 2010 +0100 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Fri Jan 08 12:26:22 2010 +0100 @@ -77,6 +77,8 @@ } declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)" +[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" + declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)" declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"