just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
authorwenzelm
Thu, 02 Nov 2023 13:05:29 +0100
changeset 78878 d03bbdd9e735
parent 78877 45d570945fe4
child 78879 2e260496a4f8
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Nov 02 12:03:30 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Thu Nov 02 13:05:29 2023 +0100
@@ -1208,15 +1208,8 @@
       if (vacuum) db.vacuum()
 
       progress.echo("Updating database " + db + " ...")
-      val errors0 = store.write_info(db, log_files, progress = progress)
-
       val errors =
-        if (ml_statistics) {
-          progress.echo("Updating database " + db + " (ML statistics) ...")
-          store.write_info(db, log_files, ml_statistics = true,
-            progress = progress, errors = errors0)
-        }
-        else errors0
+        store.write_info(db, log_files, ml_statistics = ml_statistics, progress = progress)
 
       if (errors.isEmpty) {
         for (path <- snapshot) {