pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;

--- 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