src/Pure/Tools/build.scala
changeset 66944 05df740cb54b
parent 66943 351aaaa9bacd
child 66961 f855f9aed72f
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 30 18:39:30 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 30 19:19:24 2017 +0100
     1.3 @@ -536,15 +536,18 @@
     1.4                val database = store.output_dir + store.database(name)
     1.5                database.file.delete
     1.6  
     1.7 +              val build_log =
     1.8 +                Build_Log.Log_File(name, process_result.out_lines).
     1.9 +                  parse_session_info(
    1.10 +                    command_timings = true,
    1.11 +                    theory_timings = true,
    1.12 +                    ml_statistics = true,
    1.13 +                    task_statistics = true)
    1.14 +
    1.15                using(SQLite.open_database(database))(db =>
    1.16                  store.write_session_info(db, name,
    1.17                    build_log =
    1.18 -                    Build_Log.Log_File(name, process_result.out_lines).
    1.19 -                      parse_session_info(
    1.20 -                        command_timings = true,
    1.21 -                        theory_timings = true,
    1.22 -                        ml_statistics = true,
    1.23 -                        task_statistics = true),
    1.24 +                    if (process_result.timeout) build_log.error("Timeout") else build_log,
    1.25                    build =
    1.26                      Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    1.27                        process_result.rc)))