author | wenzelm |
Tue, 21 Oct 2008 23:52:17 +0200 | |
changeset 34339 | 8c70469bc83a |
parent 34338 | b7fdb6b14e0b |
child 34340 | 19160c63b4d1 |
--- a/src/Tools/jEdit/dist-template/interface Tue Oct 21 23:16:03 2008 +0200 +++ b/src/Tools/jEdit/dist-template/interface Tue Oct 21 23:52:17 2008 +0200 @@ -91,4 +91,5 @@ export JEDIT_LOGIC JEDIT_PRINT_MODE exec "$ISABELLE_TOOL" java $JEDIT_JAVA_OPTIONS \ - -jar "$JEDIT_HOME/jedit.jar" "-settings=$ISABELLE_HOME_USER/jedit" $JEDIT_OPTIONS $FILES + -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \ + "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS $FILES