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 => {