tuned;
authorwenzelm
Sat, 20 Sep 2025 18:54:47 +0200
changeset 83199 8492484a9269
parent 83198 7f46426e69ab
child 83200 f93e95c4d3cf
tuned;
src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Sat Sep 20 18:38:45 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sat Sep 20 18:54:47 2025 +0200
@@ -279,8 +279,7 @@
             case Session.Command_Timing(props) =>
               for {
                 elapsed <- Markup.Elapsed.unapply(props)
-                elapsed_time = Time.seconds(elapsed)
-                if elapsed_time.is_notable(options.seconds("build_timing_threshold"))
+                if Time.seconds(elapsed).is_notable(options.seconds("build_timing_threshold"))
               } command_timings += props.filter(Markup.command_timing_property)
           }