# 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)