--- 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