| changeset 83248 | 1a211cab7022 |
| parent 83243 | 8f431a7a067e |
| child 83249 | 4da06d599ef6 |
--- a/src/Pure/Build/build_job.scala Mon Oct 06 18:01:21 2025 +0200 +++ b/src/Pure/Build/build_job.scala Mon Oct 06 18:53:06 2025 +0200 @@ -228,6 +228,7 @@ state.theory_snapshot(state_id, session.build_blobs) match { case None => status case Some(snapshot) => + Exn.Interrupt.expose() status.update_node(snapshot.state, snapshot.version, snapshot.node_name, threshold = editor_timing_threshold) }