removed unused property;
authorwenzelm
Sat, 11 Jul 2020 14:44:50 +0200
changeset 72241 0b1c830ebf3a
parent 72240 a851ce626b78
child 72242 c81e58a81b8c
removed unused property;
src/Pure/Tools/build.ML
--- 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