# HG changeset patch
# User wenzelm
# Date 1677527507 -3600
# Node ID 71f1abff827176b0c5616bc086455a0010c45c51
# Parent  ca3fe041f8672d98bc02bb5f3d5fb8396abb0d5e
tuned whitespace;

diff -r ca3fe041f867 -r 71f1abff8271 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Feb 27 20:39:08 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Feb 27 20:51:47 2023 +0100
@@ -1058,7 +1058,8 @@
       db: SQL.Database,
       log_name: String,
       session_names: List[String] = Nil,
-      ml_statistics: Boolean = false): Build_Info = {
+      ml_statistics: Boolean = false
+    ): Build_Info = {
       val table1 = Data.sessions_table
       val table2 = Data.ml_statistics_table