# HG changeset patch
# User wenzelm
# Date 1488142914 -3600
# Node ID 7f825cc6debf0805a235517d009d807b65ffc185
# Parent  f094e27e4902792493a1058cb7ad388eca6f8bf8
more operations;

diff -r f094e27e4902 -r 7f825cc6debf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Feb 26 22:01:14 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Feb 26 22:01:54 2017 +0100
@@ -420,6 +420,8 @@
     def finished(name: String): Boolean = get_default(name, _.finished, false)
     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
+    def ml_statistics(name: String): ML_Statistics =
+      get_default(name, entry => ML_Statistics(name, entry.ml_statistics), ML_Statistics.empty)
   }
 
   private def parse_build_info(log_file: Log_File): Build_Info =