src/Pure/Build/build.scala
changeset 83507 989304e45ad7
parent 83303 416c05062d41
--- a/src/Pure/Build/build.scala	Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/Build/build.scala	Tue Nov 04 22:09:26 2025 +0100
@@ -169,6 +169,7 @@
 
   /* build */
 
+  def progress_threshold(options: Options): Time = options.seconds("build_progress_threshold")
   def progress_detailed(options: Options): Boolean = options.bool("build_progress_detailed")
 
   def build(
@@ -433,7 +434,9 @@
       val sessions = getopts(args)
 
       val progress =
-        new Console_Progress(verbose = verbose, detailed = progress_detailed(options))
+        new Console_Progress(verbose = verbose,
+          threshold = progress_threshold(options),
+          detailed = progress_detailed(options))
 
       val ml_settings = ML_Settings(options)