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