src/Tools/jEdit/lib/Tools/jedit_client

--- a/src/Tools/jEdit/lib/Tools/jedit_client	Wed Sep 30 21:05:14 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit_client	Wed Sep 30 21:32:44 2015 +0200
@@ -85,7 +85,7 @@
 
 while [ "$#" -gt 0 ]
 do
-  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
   shift
 done
 
@@ -109,7 +109,7 @@
 if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
 then
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \
-    "-settings=$(jvmpath "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
+    "-settings=$(platform_path "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
 else
   fail "Isabelle/jEdit server \"$SERVER_NAME\" not active"
 fi