# HG changeset patch # User wenzelm # Date 1670445306 -3600 # Node ID 5af17ce5d297741253c781ae2836ae571ba94a3c # Parent 186dcfe746e33ba6ff957dd4a273d556dd0f15b1 tuned; diff -r 186dcfe746e3 -r 5af17ce5d297 src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Wed Dec 07 21:03:17 2022 +0100 +++ b/src/Pure/General/timing.scala Wed Dec 07 21:35:06 2022 +0100 @@ -65,10 +65,12 @@ case Some(f) => Timing.factor_format(f) case None => "" } - if (resources.seconds >= 3.0) + if (resources.seconds >= 3.0) { elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text - else + } + else { elapsed.message_hms + " elapsed time" + factor_text + } } override def toString: String = message