src/Pure/Admin/build_history.scala
changeset 72018 5c9984820caa
parent 72014 2550bac18b49
child 72020 ca69be5f60fe
--- 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 {