src/Pure/Tools/build.scala
changeset 66873 9953ae603a23
parent 66848 982baed14542
child 66943 351aaaa9bacd
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -537,7 +537,10 @@
     1.4                    build_log =
     1.5                      Build_Log.Log_File(name, process_result.out_lines).
     1.6                        parse_session_info(
     1.7 -                        command_timings = true, ml_statistics = true, task_statistics = true),
     1.8 +                        command_timings = true,
     1.9 +                        theory_timings = true,
    1.10 +                        ml_statistics = true,
    1.11 +                        task_statistics = true),
    1.12                    build =
    1.13                      Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    1.14                        process_result.rc)))