diff -r 679c2617f312 -r 7b1b7ac616c0 src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Tue Nov 04 17:20:20 2025 +0100 +++ b/src/Pure/Build/build_job.scala Tue Nov 04 20:11:15 2025 +0100 @@ -167,7 +167,8 @@ case None => status case Some(snapshot) => Exn.Interrupt.expose() - status.update_node(snapshot.state, snapshot.version, snapshot.node_name, + status.update_node(Date.now(), + snapshot.state, snapshot.version, snapshot.node_name, threshold = editor_timing_threshold) } })