# HG changeset patch # User wenzelm # Date 1451752680 -3600 # Node ID 2d150b6afdeb9da1a2c69d15a2a893dc23ffbc71 # Parent a77f4a9037d4dc25ee8c9ecedee82bbf67f22437 proper platform_path for Windows; diff -r a77f4a9037d4 -r 2d150b6afdeb src/Tools/jEdit/lib/Tools/jedit_client --- a/src/Tools/jEdit/lib/Tools/jedit_client Sat Jan 02 16:56:47 2016 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit_client Sat Jan 02 17:38:00 2016 +0100 @@ -108,8 +108,10 @@ if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ] then - exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \ - "-settings=$(platform_path "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}" + exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ + -jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \ + "-settings=$(platform_path "$JEDIT_SETTINGS")" \ + -server="$SERVER_NAME" -reuseview "${ARGS[@]}" else fail "Isabelle/jEdit server \"$SERVER_NAME\" not active" fi