1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 17:20:48 2013 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 17:26:58 2013 +0200
     1.3 @@ -171,7 +171,6 @@
     1.4  }
     1.5  
     1.6  declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_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  

     2.1 --- a/src/Tools/jEdit/src/jedit_main.scala	Fri Sep 06 17:20:48 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_main.scala	Fri Sep 06 17:26:58 2013 +0200
     2.3 @@ -59,6 +59,9 @@
     2.4      System.setProperty("jedit.home",
     2.5        Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
     2.6  
     2.7 +    System.setProperty("scala.home",
     2.8 +      Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
     2.9 +
    2.10      jEdit.main(jedit_options ++ jedit_settings ++ more_args)
    2.11    }
    2.12  }