| changeset 83303 | 416c05062d41 |
| parent 83266 | 2f75f2495e3e |
| child 83507 | 989304e45ad7 |
--- a/src/Pure/Build/build.scala Fri Oct 17 16:36:19 2025 +0200 +++ b/src/Pure/Build/build.scala Fri Oct 17 16:54:47 2025 +0200 @@ -169,7 +169,7 @@ /* build */ - def progress_detailed(options: Options): Boolean = options.bool("build_progress") + def progress_detailed(options: Options): Boolean = options.bool("build_progress_detailed") def build( options: Options,