--- a/src/Pure/Admin/build_history.scala Sat Jul 11 16:37:32 2020 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Jul 11 16:41:55 2020 +0200
@@ -292,12 +292,7 @@
catch { case ERROR(_) => Nil }
val session_timing =
- {
- val props = store.read_session_timing(db, session_name)
- Build.session_timing(session_name,
- Markup.Session_Timing.Threads.unapply(props) getOrElse 1,
- Markup.Timing_Properties.parse(props))
- }
+ Build.session_timing(session_name, store.read_session_timing(db, session_name))
val session_sources =
store.read_build(db, session_name).map(_.sources) match {