check source dependencies only if jedit_build component is available;
authorwenzelm
Sun, 12 Jun 2011 16:19:29 +0200
changeset 43368 0dc67b3cf8a5
parent 43367 3f1469de9e47
child 43369 4c86b3405010
check source dependencies only if jedit_build component is available;
src/Tools/jEdit/lib/Tools/jedit
--- 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