# HG changeset patch
# User wenzelm
# Date 1495048091 -7200
# Node ID 69f4dacd31cfced41d6741025add0e7abfe33280
# Parent  33b3e76114f80a5ae57bd65d4b3e14c62ebac45c
proper ml_statistics;

diff -r 33b3e76114f8 -r 69f4dacd31cf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 17 20:52:24 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 17 21:08:11 2017 +0200
@@ -800,8 +800,10 @@
 
               update_sessions(db2, log_name, read_build_info(db, log_name))
 
-              if (ml_statistics)
-                update_ml_statistics(db2, log_name, read_build_info(db, log_name))
+              if (ml_statistics) {
+                update_ml_statistics(db2, log_name,
+                  read_build_info(db, log_name, ml_statistics = true))
+              }
             }
 
             // pull_date