--- a/src/Pure/Admin/build_history.scala Sun Mar 19 12:57:29 2017 +0100
+++ b/src/Pure/Admin/build_history.scala Sun Mar 19 13:05:06 2017 +0100
@@ -230,7 +230,7 @@
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
- store.read_build_log(db, ml_statistics = true)).ml_statistics
+ store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics