src/Pure/Tools/build.scala
changeset 65318 342efc382558
parent 65317 b9f5cd845616
child 65320 52861eebf58d
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 22:11:05 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 19 11:56:56 2017 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4            try {
     1.5              using(SQLite.open_database(database))(db =>
     1.6              {
     1.7 -              val build_log = store.read_build_log(db, name, command_timings = true)
     1.8 +              val build_log = store.read_build_log(db, command_timings = true)
     1.9                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    1.10                (build_log.command_timings, session_timing)
    1.11              })
    1.12 @@ -500,10 +500,10 @@
    1.13                database.file.delete
    1.14  
    1.15                using(SQLite.open_database(database))(db =>
    1.16 -                store.write_session_info(db,
    1.17 +                store.write_session_info(db, name,
    1.18                    build_log =
    1.19                      Build_Log.Log_File(name, process_result.out_lines).
    1.20 -                      parse_session_info(name,
    1.21 +                      parse_session_info(
    1.22                          command_timings = true, ml_statistics = true, task_statistics = true),
    1.23                    build =
    1.24                      Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))