# HG changeset patch
# User wenzelm
# Date 1700318686 -3600
# Node ID 417b490c9b89ab01ee832f3d947f02a7c10f9fd5
# Parent  295aa95cbff92bc1aad34f1eab468a8d32ecaac0
proper ml_statistics (amending aeb511a520f4);

diff -r 295aa95cbff9 -r 417b490c9b89 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Nov 17 10:11:15 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 18 15:44:46 2023 +0100
@@ -1044,8 +1044,7 @@
       }
 
       val ml_statistics_status =
-        if (ml_statistics) Nil
-        else {
+        if (ml_statistics) {
           List(
             new Table_Status(private_data.ml_statistics_table) {
               override def update_db(db: SQL.Database, log_file: Log_File): Unit =
@@ -1053,6 +1052,7 @@
                   log_file.parse_build_info(ml_statistics = true))
             })
         }
+        else Nil
       val status =
         List(
           new Table_Status(private_data.meta_info_table) {