src/Pure/System/process_result.ML

--- a/src/Pure/System/process_result.ML	Mon Feb 22 18:16:56 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 18:19:38 2021 +0100
@@ -16,6 +16,7 @@
   val out_lines: T -> string list
   val err_lines: T -> string list
   val timing: T -> Timing.timing
+  val timing_elapsed: T -> Time.time
   val out: T -> string
   val err: T -> string
   val ok: T -> bool
@@ -40,7 +41,9 @@
 val rc = #rc o rep;
 val out_lines = #out_lines o rep;
 val err_lines = #err_lines o rep;
+
 val timing = #timing o rep;
+val timing_elapsed = #elapsed o timing;
 
 end;