clarified no_build vs. verbose;
authorwenzelm
Tue, 24 Jul 2012 12:47:48 +0200
changeset 48471 9d5ce7f1002d
parent 48470 7483aa690b4f
child 48472 6ebb6cdd36a5
clarified no_build vs. verbose;
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)) {