src/Pure/Build/build_job.scala
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