proper ml_statistics (amending aeb511a520f4);
authorwenzelm
Sat, 18 Nov 2023 15:44:46 +0100
changeset 78984 417b490c9b89
parent 78983 295aa95cbff9
child 78985 24e686fe043e
proper ml_statistics (amending aeb511a520f4);
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) {