| changeset 83504 | 24998f6c9c15 |
| parent 83503 | 7b1b7ac616c0 |
| child 83507 | 989304e45ad7 |
--- a/src/Pure/Build/build_job.scala Tue Nov 04 20:11:15 2025 +0100 +++ b/src/Pure/Build/build_job.scala Tue Nov 04 20:16:21 2025 +0100 @@ -167,7 +167,7 @@ case None => status case Some(snapshot) => Exn.Interrupt.expose() - status.update_node(Date.now(), + status.update_node(progress.now(), snapshot.state, snapshot.version, snapshot.node_name, threshold = editor_timing_threshold) }