clarified no_build vs. verbose;
--- 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)) {