define scala.home, for more robust startup of Scala tools, notably the compiler;
authorwenzelm
Fri, 08 Jan 2010 12:26:22 +0100
changeset 34846eb8806a2e348
parent 34845 2f6f9b6099b2
child 34847 92ea2174ea78
define scala.home, for more robust startup of Scala tools, notably the compiler;
src/Tools/jEdit/dist-template/lib/Tools/jedit
     1.1 --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Fri Jan 08 12:25:37 2010 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Fri Jan 08 12:26:22 2010 +0100
     1.3 @@ -77,6 +77,8 @@
     1.4  }
     1.5  
     1.6  declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
     1.7 +[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
     1.8 +
     1.9  declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
    1.10  
    1.11  declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"