equal
deleted
inserted
replaced
205 pushd "$JEDIT_HOME" >/dev/null || failed |
205 pushd "$JEDIT_HOME" >/dev/null || failed |
206 |
206 |
207 JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar" |
207 JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar" |
208 |
208 |
209 JEDIT_JARS=( |
209 JEDIT_JARS=( |
|
210 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Code2HTML.jar" |
|
211 "$ISABELLE_JEDIT_BUILD_HOME/contrib/CommonControls.jar" |
210 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar" |
212 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar" |
211 "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar" |
213 "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar" |
212 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar" |
214 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar" |
|
215 "$ISABELLE_JEDIT_BUILD_HOME/contrib/kappalayout.jar" |
213 "$ISABELLE_JEDIT_BUILD_HOME/contrib/MacOSX.jar" |
216 "$ISABELLE_JEDIT_BUILD_HOME/contrib/MacOSX.jar" |
|
217 "$ISABELLE_JEDIT_BUILD_HOME/contrib/Navigator.jar" |
214 "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar" |
218 "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar" |
215 "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar" |
219 "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar" |
216 "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar" |
220 "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar" |
217 ) |
221 ) |
218 |
222 |