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 + ")" }