# 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