--- 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)