src/Pure/Admin/jenkins.scala
changeset 65935 73c099fa96a4
parent 65896 18f5014331a1
child 66880 486f4af28db9
--- a/src/Pure/Admin/jenkins.scala	Fri May 26 15:19:21 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Fri May 26 15:28:46 2017 +0200
@@ -84,8 +84,7 @@
         case Some(url) =>
           Isabelle_System.with_tmp_file(session_name, "db") { database =>
             Bytes.write(database, Bytes.read(url))
-            using(SQLite.open_database(database))(db =>
-              store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
+            using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name))
           }
         case None =>
           get_log("gz") match {