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