src/Pure/Admin/build_history.scala
changeset 65935 73c099fa96a4
parent 65931 83c44969f431
child 65937 fde7b5d209d5
--- a/src/Pure/Admin/build_history.scala	Fri May 26 15:19:21 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri May 26 15:28:46 2017 +0200
@@ -241,7 +241,7 @@
             val properties =
               if (database.is_file) {
                 using(SQLite.open_database(database))(db =>
-                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
+                  store.read_ml_statistics(db, session_name))
               }
               else if (log_gz.is_file) {
                 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics