src/Pure/Tools/build.scala
changeset 71894 ab21876c30c1
parent 71879 fe7ee970c425
child 71895 7a39036d5a19
--- a/src/Pure/Tools/build.scala	Mon May 25 22:37:22 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 26 11:17:10 2020 +0200
@@ -718,7 +718,7 @@
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
-                  if (verbose) progress.echo("Skipping " + session_name + " ...")
+                  progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))