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