# HG changeset patch
# User wenzelm
# Date 1494358054 -7200
# Node ID c60b1a2c3abc4a7b241046b9293fd7c56bd8f5e6
# Parent  a880f41a8d0fe09a05aa47a91ffe1e5237b3d12a
clarified;

diff -r a880f41a8d0f -r c60b1a2c3abc src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 09 21:25:32 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:27:34 2017 +0200
@@ -61,8 +61,10 @@
   sealed case class Data_Entry(name: String, hosts: List[String], sessions: List[Session])
   sealed case class Session(name: String, threads: Int, entries: List[Entry])
   {
-    def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing
-    def ml_timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.ml_timing
+    require(entries.nonEmpty)
+
+    def timing: Timing = entries.head.timing
+    def ml_timing: Timing = entries.head.ml_timing
     def order: Long = - timing.elapsed.ms
 
     def check_timing: Boolean = entries.length >= 3