src/Pure/Concurrent/bash.scala
changeset 62399 36e885190439
parent 62304 e7a52a838a23
child 62400 833af0d6d469
--- a/src/Pure/Concurrent/bash.scala	Wed Feb 24 16:00:57 2016 +0000
+++ b/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:03:24 2016 +0100
@@ -23,10 +23,13 @@
     def error(s: String, err_rc: Int = 0): Result =
       copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
 
+    def ok: Boolean = rc == 0
+    def interrupted: Boolean = rc == Exn.Interrupt.return_code
+
     def check: Result =
-      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) Library.error(err)
-      else this
+      if (ok) this
+      else if (interrupted) throw Exn.Interrupt()
+      else Library.error(err)
 
     def print: Result =
     {