--- 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) {