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("""\""") + a)) } final class Statistics private(