changeset 68927 | 01f46a4b22b4 |
parent 68091 | 0c7820590236 |
child 71631 | 3f02bc5a5a03 |
--- a/src/Pure/System/process_result.scala Fri Sep 07 17:08:47 2018 +0200 +++ b/src/Pure/System/process_result.scala Fri Sep 07 19:11:16 2018 +0200 @@ -23,6 +23,8 @@ def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code + def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) + def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt()