tuned whitespace;
authorwenzelm
Mon, 27 Feb 2023 20:51:47 +0100
changeset 77405 71f1abff8271
parent 77404 ca3fe041f867
child 77408 8fe30123aaab
tuned whitespace;
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