src/Pure/Admin/build_log.scala
changeset 65052 7f825cc6debf
parent 64341 45b6faeee56d
child 65276 fa1a5efee2ec
     1.1 --- a/src/Pure/Admin/build_log.scala	Sun Feb 26 22:01:14 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sun Feb 26 22:01:54 2017 +0100
     1.3 @@ -420,6 +420,8 @@
     1.4      def finished(name: String): Boolean = get_default(name, _.finished, false)
     1.5      def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
     1.6      def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
     1.7 +    def ml_statistics(name: String): ML_Statistics =
     1.8 +      get_default(name, entry => ML_Statistics(name, entry.ml_statistics), ML_Statistics.empty)
     1.9    }
    1.10  
    1.11    private def parse_build_info(log_file: Log_File): Build_Info =