--- a/src/Pure/Tools/build.scala Mon Oct 30 18:39:30 2017 +0100
+++ b/src/Pure/Tools/build.scala Mon Oct 30 19:19:24 2017 +0100
@@ -536,15 +536,18 @@
val database = store.output_dir + store.database(name)
database.file.delete
+ val build_log =
+ Build_Log.Log_File(name, process_result.out_lines).
+ parse_session_info(
+ command_timings = true,
+ theory_timings = true,
+ ml_statistics = true,
+ task_statistics = true)
+
using(SQLite.open_database(database))(db =>
store.write_session_info(db, name,
build_log =
- Build_Log.Log_File(name, process_result.out_lines).
- parse_session_info(
- command_timings = true,
- theory_timings = true,
- ml_statistics = true,
- task_statistics = true),
+ if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
process_result.rc)))