# 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