--- a/src/Pure/System/process_result.scala Wed Mar 09 14:24:16 2016 +0100
+++ b/src/Pure/System/process_result.scala Wed Mar 09 14:54:51 2016 +0100
@@ -10,13 +10,14 @@
rc: Int,
out_lines: List[String] = Nil,
err_lines: List[String] = Nil,
- timeout: Option[Time] = None)
+ timeout: Boolean = false,
+ timing: Timing = Timing.zero)
{
def out: String = cat_lines(out_lines)
def err: String = cat_lines(err_lines)
def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
- def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
+ def was_timeout: Process_Result = copy(rc = 1, timeout = true)
def ok: Boolean = rc == 0
def interrupted: Boolean = rc == Exn.Interrupt.return_code