src/Pure/Tools/build.scala
changeset 74782 0a87ea7eb76f
parent 74770 32c2587cda4f
child 74798 507f50dbeb79
--- a/src/Pure/Tools/build.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -161,7 +161,7 @@
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
-    val timing = Markup.Timing_Properties.parse(props)
+    val timing = Markup.Timing_Properties.get(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }