src/Pure/Tools/build.scala
changeset 64082 d57c7295f601
parent 64081 38bb09ed965b
child 64115 68619fa37ca7
--- a/src/Pure/Tools/build.scala	Fri Oct 07 11:45:30 2016 +0200
+++ b/src/Pure/Tools/build.scala	Fri Oct 07 13:58:10 2016 +0200
@@ -477,7 +477,7 @@
       }
 
       try {
-        val info = Build_Log.Log_File(name, text).parse_session_info(name, false)
+        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }