# HG changeset patch
# User wenzelm
# Date 1343325453 -7200
# Node ID 784c6f63d79ce2ea3f9a0d11940b07dde3aee95a
# Parent  4ee8d70cd5a35ea4e399435d7da98fd2242c0db5
proper all_current, which regards parent status as well;

diff -r 4ee8d70cd5a3 -r 784c6f63d79c src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 26 19:41:05 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 26 19:57:33 2012 +0200
@@ -502,10 +502,12 @@
       { // check/start next job
         pending.dequeue(running.isDefinedAt(_)) match {
           case Some((name, info)) =>
+            val parents_ok = info.parent.map(results(_)).forall(_ == 0)
+
             val output = output_dir + Path.basic(name)
             val do_output = build_heap || queue.is_inner(name)
 
-            val current =
+            val all_current =
             {
               input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
                 case Some(dir) =>
@@ -515,10 +517,11 @@
                   }
                 case None => false
               }
-            }
-            if (current || no_build)
-              loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
-            else if (info.parent.map(results(_)).forall(_ == 0)) {
+            } && parents_ok
+
+            if (all_current || no_build)
+              loop(pending - name, running, results + (name -> (if (all_current) 0 else 1)))
+            else if (parents_ok) {
               echo((if (do_output) "Building " else "Running ") + name + " ...")
               val job =
                 start_job(name, info, output, do_output, info.options, timing, verbose, browser_info)