| changeset 83299 | 7d8713e1890b |
| parent 83295 | 094d96f05cba |
| child 83301 | 88e33d16f2de |
--- a/src/Pure/Build/build_job.scala Fri Oct 17 15:19:01 2025 +0200 +++ b/src/Pure/Build/build_job.scala Fri Oct 17 15:28:55 2025 +0200 @@ -214,7 +214,7 @@ val elapsed = Time.seconds(Markup.Elapsed.get(props)) if (elapsed.is_notable(build_timing_threshold)) { write_process_output( - Protocol.Command_Timing_Marker(props.filter(Markup.command_timing_property))) + Protocol.Command_Timing_Marker(props.filter(Markup.command_timing_export))) } nodes_changed += state_id