src/Pure/Admin/build_history.scala
changeset 65320 52861eebf58d
parent 65318 342efc382558
child 65588 b0d8d97198b3
--- 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