src/Pure/Tools/build_job.scala
changeset 74067 0b1462ce5fda
parent 73897 0ddb5de0506e
child 74144 f9f6a31cc99c
--- a/src/Pure/Tools/build_job.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -503,7 +503,7 @@
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
         case Exn.Exn(Exn.Interrupt()) =>
-          if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
+          if (result.ok) result.copy(rc = Process_Result.interrupt_rc) else result
         case Exn.Exn(exn) => throw exn
       }
     }