author | wenzelm |
Wed, 17 May 2017 21:08:11 +0200 | |
changeset 65856 | 69f4dacd31cf |
parent 65855 | 33b3e76114f8 |
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