src/Pure/Admin/build_log.scala
changeset 65856 69f4dacd31cf
parent 65853 cf24cc0b0a47
child 65857 5d29d93766ef
--- 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