src/Pure/System/process_result.scala
changeset 62569 5db10482f4cf
parent 62553 d2e0d626fb96
child 64024 3dd92c391eca
--- 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