# HG changeset patch
# User wenzelm
# Date 1739109275 -3600
# Node ID f6460ae54866405077fcd65e98e7db4da5adcf2a
# Parent  1eda03781f76132a1ddff690dfaebfc5acff7394
tuned: more robust Isabelle symbols;

diff -r 1eda03781f76 -r f6460ae54866 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(