# HG changeset patch # User wenzelm # Date 1308434624 -7200 # Node ID 71b7a535cf9619d0a1d85c311e255d6973f5ca33 # Parent 3c9696efe6b4506037274bb6e30e6e7369562b6e tuned; diff -r 3c9696efe6b4 -r 71b7a535cf96 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sat Jun 18 23:51:22 2011 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Jun 19 00:03:44 2011 +0200 @@ -182,9 +182,9 @@ OUTDATED=true else if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then - declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$PURE_JAR" "$JEDIT_JAR" "${JEDIT_JARS[@]}") + declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}") else - declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$PURE_JAR") + declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}") fi for DEP in "${DEPS[@]}" do