diff -r d892f6d66402 -r c7ab83a0c564 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Wed Nov 11 21:00:14 2020 +0100 +++ b/src/Pure/Admin/build_history.scala Wed Nov 11 21:04:22 2020 +0100 @@ -358,8 +358,8 @@ else None }) - build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...") - File.write_xz(log_path.ext("xz"), + build_out_progress.echo("Writing log file " + log_path.xz + " ...") + File.write_xz(log_path.xz, terminate_lines( Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: @@ -377,7 +377,7 @@ first_build = false - (build_result, log_path.ext("xz")) + (build_result, log_path.xz) } }