# HG changeset patch
# User wenzelm
# Date 1343126868 -7200
# Node ID 9d5ce7f1002d88c648a94429353af0a423ef951c
# Parent  7483aa690b4f387289d6e0cd19d97906db00f39a
clarified no_build vs. verbose;

diff -r 7483aa690b4f -r 9d5ce7f1002d src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 24 12:38:33 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 12:47:48 2012 +0200
@@ -451,8 +451,8 @@
       else if (running.size < (max_jobs max 1)) {
         pending.dequeue(running.isDefinedAt(_)) match {
           case Some((name, info)) =>
-            if (no_build && verbose) {
-              echo(name + " in " + info.dir)
+            if (no_build) {
+              if (verbose) echo(name + " in " + info.dir)
               loop(pending - name, running, results + (name -> 0))
             }
             else if (info.parent.map(results(_)).forall(_ == 0)) {