src/Pure/System/bash.scala
changeset 65317 b9f5cd845616
parent 65316 c0fb8405416c
child 67200 d49727160f0a
--- a/src/Pure/System/bash.scala	Sat Mar 18 21:40:47 2017 +0100
+++ b/src/Pure/System/bash.scala	Sat Mar 18 22:11:05 2017 +0100
@@ -72,6 +72,7 @@
   {
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
+    def get_timing: Timing = timing.value getOrElse Timing.zero
 
     private val script_file = Isabelle_System.tmp_file("bash_script")
     File.write(script_file, script)
@@ -199,7 +200,7 @@
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
+      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
     }
   }
 }