src/Pure/Concurrent/bash.scala
changeset 62303 f868f12f9419
parent 62302 236e1ea5a197
child 62304 e7a52a838a23
--- a/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:03:32 2016 +0100
@@ -19,12 +19,13 @@
   {
     def out: String = cat_lines(out_lines)
     def err: String = cat_lines(err_lines)
-    def add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
-    def set_rc(i: Int): Result = copy(rc = i)
+
+    def error(s: String, err_rc: Int = 0): Result =
+      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
 
-    def check_error: Result =
+    def check: Result =
       if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-      else if (rc != 0) error(err)
+      else if (rc != 0) Library.error(err)
       else this
 
     def print: Result =