src/Pure/Admin/build_status.scala
changeset 71894 ab21876c30c1
parent 71726 a5fda30edae2
child 72375 e48d93811ed7
--- a/src/Pure/Admin/build_status.scala	Mon May 25 22:37:22 2020 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 26 11:17:10 2020 +0200
@@ -250,7 +250,7 @@
         val Threads_Option = """threads\s*=\s*(\d+)""".r
 
         val sql = profile.select(options, columns, only_sessions)
-        if (verbose) progress.echo(sql)
+        progress.echo_if(verbose, sql)
 
         db.using_statement(sql)(stmt =>
         {