equal
deleted
inserted
replaced
259 "CommonControls.jar" |
259 "CommonControls.jar" |
260 "Console.jar" |
260 "Console.jar" |
261 "ErrorList.jar" |
261 "ErrorList.jar" |
262 "Highlight.jar" |
262 "Highlight.jar" |
263 "kappalayout.jar" |
263 "kappalayout.jar" |
264 "MacOSX.jar" |
|
265 "Navigator.jar" |
264 "Navigator.jar" |
266 "SideKick.jar" |
265 "SideKick.jar" |
267 "idea-icons.jar" |
266 "idea-icons.jar" |
268 "jsr305-2.0.0.jar" |
267 "jsr305-2.0.0.jar" |
269 ) |
268 ) |
388 compile_sources "${SOURCES[@]}" |
387 compile_sources "${SOURCES[@]}" |
389 make_jar "$TARGET_JAR" |
388 make_jar "$TARGET_JAR" |
390 |
389 |
391 target_shasum > "$TARGET_SHASUM" |
390 target_shasum > "$TARGET_SHASUM" |
392 |
391 |
393 cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.5.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf" |
392 cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6pre1manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf" |
394 cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes" |
393 cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes" |
395 cat > "$TARGET_DIR/doc/Contents" <<EOF |
394 cat > "$TARGET_DIR/doc/Contents" <<EOF |
396 Original jEdit Documentation |
395 Original jEdit Documentation |
397 jedit-manual jEdit 5.5 User's Guide |
396 jedit-manual jEdit 5.6 User's Guide |
398 jedit-changes jEdit 5.5 Version History |
397 jedit-changes jEdit 5.6 Version History |
399 |
398 |
400 EOF |
399 EOF |
401 |
400 |
402 fi |
401 fi |
403 |
402 |