# 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