--- a/src/Tools/jEdit/lib/Tools/jedit Sat Jun 11 16:05:17 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Jun 12 16:19:29 2011 +0200
@@ -169,11 +169,15 @@
OUTDATED=true
else
OUTDATED=false
- for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
- do
- [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
- [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
- done
+ if [ ! -e "$TARGET" ]; then
+ OUTDATED=true
+ elif [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+ for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ do
+ [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
+ [ "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
+ done
+ fi
fi