# HG changeset patch
# User wenzelm
# Date 1335105146 -7200
# Node ID cf5fe7eb6793a20dd809cb51b2ecd7bb154aa1e7
# Parent  2cbf029abca9ea55ae09335624d52436ea088a15
pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;

diff -r 2cbf029abca9 -r cf5fe7eb6793 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 16:08:10 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 16:32:26 2012 +0200
@@ -189,8 +189,10 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
+      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
     else
-      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+      declare -a DEPS=()
     fi
     for DEP in "${DEPS[@]}"
     do