| 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