equal
deleted
inserted
replaced
106 |
106 |
107 "$ISABELLE_TOOL" jedit -b || exit $? |
107 "$ISABELLE_TOOL" jedit -b || exit $? |
108 |
108 |
109 if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ] |
109 if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ] |
110 then |
110 then |
111 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \ |
111 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ |
112 "-settings=$(platform_path "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}" |
112 -jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \ |
|
113 "-settings=$(platform_path "$JEDIT_SETTINGS")" \ |
|
114 -server="$SERVER_NAME" -reuseview "${ARGS[@]}" |
113 else |
115 else |
114 fail "Isabelle/jEdit server \"$SERVER_NAME\" not active" |
116 fail "Isabelle/jEdit server \"$SERVER_NAME\" not active" |
115 fi |
117 fi |