--- a/src/Pure/Build/build.scala Tue Sep 23 12:36:36 2025 +0200
+++ b/src/Pure/Build/build.scala Tue Sep 23 13:11:52 2025 +0200
@@ -22,6 +22,16 @@
def engine_name(options: Options): String = options.string("build_engine")
+ /* detailed build progress */
+
+ class Build_Progress(options: Options, verbose: Boolean = false)
+ extends Console_Progress(verbose = verbose) {
+ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
+ if (options.bool("build_progress")) {
+ output(nodes_status.message.copy(verbose = false))
+ }
+ }
+
/* context */
@@ -431,7 +441,7 @@
val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Build_Progress(options, verbose = verbose)
val ml_settings = ML_Settings(options)