# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719990879 -7200
# Node ID 5b539d1d357776931da0e3c6c29c3f6e32c72333
# Parent  2136ecf06a4cf825166155c924cd2d276ab4f33b
clarified: control verbosity;

diff -r 2136ecf06a4c -r 5b539d1d3577 src/Pure/Build/build_ci.scala
--- a/src/Pure/Build/build_ci.scala	Tue Jul 02 23:29:46 2024 +0200
+++ b/src/Pure/Build/build_ci.scala	Wed Jul 03 09:14:39 2024 +0200
@@ -113,7 +113,8 @@
     hook: Hook = none,
     extra_components: List[String] = Nil,
     other_settings: List[String] = Nil,
-    trigger: Trigger = On_Commit
+    trigger: Trigger = On_Commit,
+    verbose: Boolean = false
   ) {
     override def toString: String = name
 
@@ -266,7 +267,7 @@
           case _ => getopts.usage()
         }
 
-      val progress = new Console_Progress(verbose = true)
+      val progress = new Console_Progress(verbose = job.verbose)
 
       build_ci(options, job, url = url, build_hosts = build_hosts.toList, progress = progress)
     })