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 } }