src/Pure/Admin/build_status.scala
changeset 65795 c60b1a2c3abc
parent 65794 a880f41a8d0f
child 65796 7d1c5150af70
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 21:25:32 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:27:34 2017 +0200
     1.3 @@ -61,8 +61,10 @@
     1.4    sealed case class Data_Entry(name: String, hosts: List[String], sessions: List[Session])
     1.5    sealed case class Session(name: String, threads: Int, entries: List[Entry])
     1.6    {
     1.7 -    def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing
     1.8 -    def ml_timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.ml_timing
     1.9 +    require(entries.nonEmpty)
    1.10 +
    1.11 +    def timing: Timing = entries.head.timing
    1.12 +    def ml_timing: Timing = entries.head.ml_timing
    1.13      def order: Long = - timing.elapsed.ms
    1.14  
    1.15      def check_timing: Boolean = entries.length >= 3