# HG changeset patch
# User wenzelm
# Date 1594478252 -7200
# Node ID 17a41deb595040610bf4c2ff499fde365395bd3a
# Parent  5469bacf5573294e41cfec6a7d2899b6669eaff7
tuned;

diff -r 5469bacf5573 -r 17a41deb5950 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 16:32:25 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 16:37:32 2020 +0200
@@ -650,6 +650,13 @@
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
+            val build_log =
+              Build_Log.Log_File(session_name, process_result.out_lines).
+                parse_session_info(
+                  command_timings = true,
+                  theory_timings = true,
+                  ml_statistics = true,
+                  task_statistics = true)
 
             // write log file
             if (process_result.ok) {
@@ -658,23 +665,13 @@
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
-            {
-              val build_log =
-                Build_Log.Log_File(session_name, process_result.out_lines).
-                  parse_session_info(
-                    command_timings = true,
-                    theory_timings = true,
-                    ml_statistics = true,
-                    task_statistics = true)
-
-              using(store.open_database(session_name, output = true))(db =>
-                store.write_session_info(db, session_name,
-                  build_log =
-                    if (process_result.timeout) build_log.error("Timeout") else build_log,
-                  build =
-                    Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
-                      process_result.rc)))
-            }
+            using(store.open_database(session_name, output = true))(db =>
+              store.write_session_info(db, session_name,
+                build_log =
+                  if (process_result.timeout) build_log.error("Timeout") else build_log,
+                build =
+                  Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
+                    process_result.rc)))
 
             // messages
             process_result.err_lines.foreach(progress.echo)