# HG changeset patch
# User wenzelm
# Date 1689246640 -7200
# Node ID a041d49736f23df039285025097bba662959b867
# Parent  007b04dc6f96e91c54413f410610daafa9c89725
tuned output;

diff -r 007b04dc6f96 -r a041d49736f2 src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Thu Jul 13 13:04:15 2023 +0200
+++ b/src/Pure/Tools/profiling.scala	Thu Jul 13 13:10:40 2023 +0200
@@ -110,14 +110,14 @@
         "locales",
         "locale_thms",
         "global_thms",
-        "locale_thms_percentage",
-        "global_thms_percentage",
+        "locale_thms%",
+        "global_thms%",
         "heap_size",
-        "thys_id_size_percentage",
-        "thms_id_size_percentage",
-        "terms_size_percentage",
-        "types_size_percentage",
-        "spaces_size_percentage")
+        "thys_id_size%",
+        "thms_id_size%",
+        "terms_size%",
+        "types_size%",
+        "spaces_size%")
 
     def header: List[String] = "session" :: header0 ::: header0.map(_ + "_cumulative")
   }