--- a/src/Pure/System/process_result.scala Wed Oct 26 15:21:16 2016 +0200
+++ b/src/Pure/System/process_result.scala Wed Oct 26 16:04:05 2016 +0200
@@ -22,11 +22,13 @@
def ok: Boolean = rc == 0
def interrupted: Boolean = rc == Exn.Interrupt.return_code
- def check: Process_Result =
- if (ok) this
+ def check_rc(pred: Int => Boolean): Process_Result =
+ if (pred(rc)) this
else if (interrupted) throw Exn.Interrupt()
else Exn.error(err)
+ def check: Process_Result = check_rc(_ == 0)
+
def print: Process_Result =
{
Output.warning(err)