src/Pure/Concurrent/bash.scala
changeset 62303 f868f12f9419
parent 62302 236e1ea5a197
child 62304 e7a52a838a23
     1.1 --- a/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 12:03:32 2016 +0100
     1.3 @@ -19,12 +19,13 @@
     1.4    {
     1.5      def out: String = cat_lines(out_lines)
     1.6      def err: String = cat_lines(err_lines)
     1.7 -    def add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
     1.8 -    def set_rc(i: Int): Result = copy(rc = i)
     1.9  
    1.10 -    def check_error: Result =
    1.11 +    def error(s: String, err_rc: Int = 0): Result =
    1.12 +      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
    1.13 +
    1.14 +    def check: Result =
    1.15        if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    1.16 -      else if (rc != 0) error(err)
    1.17 +      else if (rc != 0) Library.error(err)
    1.18        else this
    1.19  
    1.20      def print: Result =