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) }