src/Pure/Concurrent/bash.scala
changeset 62302 236e1ea5a197
parent 62296 b04a5ddd6121
child 62303 f868f12f9419
     1.1 --- a/src/Pure/Concurrent/bash.scala	Sat Feb 13 20:41:56 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Sun Feb 14 11:52:27 2016 +0100
     1.3 @@ -26,6 +26,13 @@
     1.4        if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
     1.5        else if (rc != 0) error(err)
     1.6        else this
     1.7 +
     1.8 +    def print: Result =
     1.9 +    {
    1.10 +      Output.warning(Library.trim_line(err))
    1.11 +      Output.writeln(Library.trim_line(out))
    1.12 +      Result(Nil, Nil, rc)
    1.13 +    }
    1.14    }
    1.15  
    1.16