diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/Build/build.scala --- 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)