--- a/src/Pure/Tools/build.ML Sat Jul 11 06:21:04 2020 +0000
+++ b/src/Pure/Tools/build.ML Sat Jul 11 14:44:50 2020 +0200
@@ -56,8 +56,7 @@
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
|> Real.fmt (StringCvt.FIX (SOME 2));
- val timing_props =
- [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
+ val timing_props = [("threads", threads)] @ Markup.timing_properties timing;
val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
val _ =
if verbose then