proper ml_statistics;
authorwenzelm
Wed, 17 May 2017 21:08:11 +0200
changeset 65856 69f4dacd31cf
parent 65855 33b3e76114f8
child 65857 5d29d93766ef
proper ml_statistics;
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