src/Pure/Build/build_job.scala
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)
                     }