--- 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