# HG changeset patch
# User wenzelm
# Date 1594480106 -7200
# Node ID ca69be5f60fe2f3ece3e0b28c9fa51333fc59612
# Parent  940195fbb2823e5c309de323e99374a09a6f81dc
clarified messages: avoid duplicate Timing;

diff -r 940195fbb282 -r ca69be5f60fe src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jul 11 16:58:38 2020 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jul 11 17:08:26 2020 +0200
@@ -291,9 +291,6 @@
                   }
                   catch { case ERROR(_) => Nil }
 
-                val session_timing =
-                  Build.session_timing(session_name, store.read_session_timing(db, session_name))
-
                 val session_sources =
                   store.read_build(db, session_name).map(_.sources) match {
                     case Some(sources) if sources.length == SHA1.digest_length =>
@@ -301,7 +298,7 @@
                     case _ => Nil
                   }
 
-                theory_timings ::: List(session_timing) ::: session_sources
+                theory_timings ::: session_sources
               })
             }
             else Nil