# HG changeset patch # User wenzelm # Date 1378481218 -7200 # Node ID 63958e9e0073c5e984e5588be0e7cf9d59a5e69c # Parent b99d006afbfe926c007afc9129f5e57340a9180a prefer Isabelle/Scala over bash; actual platform_path (in contrast to eb8806a2e348); diff -r b99d006afbfe -r 63958e9e0073 src/Tools/jEdit/lib/Tools/jedit --- 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)" diff -r b99d006afbfe -r 63958e9e0073 src/Tools/jEdit/src/jedit_main.scala --- a/src/Tools/jEdit/src/jedit_main.scala Fri Sep 06 17:20:48 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_main.scala Fri Sep 06 17:26:58 2013 +0200 @@ -59,6 +59,9 @@ System.setProperty("jedit.home", Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist"))) + System.setProperty("scala.home", + Isabelle_System.platform_path(Path.explode("$SCALA_HOME"))) + jEdit.main(jedit_options ++ jedit_settings ++ more_args) } }