1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Jun 11 16:05:17 2011 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Jun 12 16:19:29 2011 +0200
     1.3 @@ -169,11 +169,15 @@
     1.4    OUTDATED=true
     1.5  else
     1.6    OUTDATED=false
     1.7 -  for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
     1.8 -  do
     1.9 -    [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
    1.10 -    [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
    1.11 -  done
    1.12 +  if [ ! -e "$TARGET" ]; then
    1.13 +    OUTDATED=true
    1.14 +  elif [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
    1.15 +    for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
    1.16 +    do
    1.17 +      [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
    1.18 +      [ "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
    1.19 +    done
    1.20 +  fi
    1.21  fi
    1.22  
    1.23