diff -r 37b61794a93a -r 2ecfd436903b src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Wed Sep 24 17:41:36 2025 +0200 +++ b/src/Pure/Build/build_job.scala Wed Sep 24 21:52:03 2025 +0200 @@ -239,7 +239,8 @@ val result = if (nodes_changed.isEmpty) None else { - Some(Progress.Nodes_Status(nodes_domain, nodes_status1, session = session_name)) + Some(Progress.Nodes_Status( + nodes_domain, nodes_status1, session = session_name, old = Some(nodes_status))) } nodes_changed = Set.empty