src/Pure/Tools/profiling.scala

--- a/src/Pure/Tools/profiling.scala	Sun Feb 09 14:54:23 2025 +0100
+++ b/src/Pure/Tools/profiling.scala	Sun Feb 09 14:54:35 2025 +0100
@@ -128,7 +128,7 @@
         "spaces_size%")
 
     def header: List[String] =
-      "session" :: header0.flatMap(a => List(a, "\u2211" + a))
+      "session" :: header0.flatMap(a => List(a, Symbol.decode("""\<Sum>""") + a))
   }
 
   final class Statistics private(