--- a/src/Pure/Tools/build.scala Sat Jul 11 16:37:32 2020 +0200
+++ b/src/Pure/Tools/build.scala Sat Jul 11 16:41:55 2020 +0200
@@ -490,6 +490,11 @@
def session_timing(session_name: String, threads: Int, timing: Timing): String =
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
+ def session_timing(session_name: String, props: Properties.T): String =
+ session_timing(session_name,
+ Markup.Session_Timing.Threads.unapply(props) getOrElse 1,
+ Markup.Timing_Properties.parse(props))
+
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,