equal
deleted
inserted
replaced
8 |
8 |
9 final case class Process_Result( |
9 final case class Process_Result( |
10 rc: Int, |
10 rc: Int, |
11 out_lines: List[String] = Nil, |
11 out_lines: List[String] = Nil, |
12 err_lines: List[String] = Nil, |
12 err_lines: List[String] = Nil, |
13 timeout: Option[Time] = None) |
13 timeout: Boolean = false, |
|
14 timing: Timing = Timing.zero) |
14 { |
15 { |
15 def out: String = cat_lines(out_lines) |
16 def out: String = cat_lines(out_lines) |
16 def err: String = cat_lines(err_lines) |
17 def err: String = cat_lines(err_lines) |
17 def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s)) |
18 def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s)) |
18 |
19 |
19 def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t)) |
20 def was_timeout: Process_Result = copy(rc = 1, timeout = true) |
20 |
21 |
21 def ok: Boolean = rc == 0 |
22 def ok: Boolean = rc == 0 |
22 def interrupted: Boolean = rc == Exn.Interrupt.return_code |
23 def interrupted: Boolean = rc == Exn.Interrupt.return_code |
23 |
24 |
24 def check: Process_Result = |
25 def check: Process_Result = |