src/Pure/Build/build_job.scala
changeset 83227 2ecfd436903b
parent 83224 14d83daeaafc
child 83243 8f431a7a067e
--- 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