From 923cac500a8292c94de98d501019e6e100652410 Mon Sep 17 00:00:00 2001
From: Sylvain Pion <Sylvain.Pion@sophia.inria.fr>
Date: Mon, 7 Aug 2006 15:45:23 +0000
Subject: [PATCH] output formatting improvement

---
 Filtered_kernel/developer_scripts/profile_cleanup | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Filtered_kernel/developer_scripts/profile_cleanup b/Filtered_kernel/developer_scripts/profile_cleanup
index ae854063a4b..f990838684a 100755
--- a/Filtered_kernel/developer_scripts/profile_cleanup
+++ b/Filtered_kernel/developer_scripts/profile_cleanup
@@ -32,6 +32,6 @@ cat $@ | sed -e 's/CGAL:://g' \
              -e 's/<LK >//g' \
              -e 's/<EK >//g' \
              -e 's/<IK >//g' \
-             -e 's/ (.*)//g' \
+             -e 's/ (.*)/ /g' \
        | grep Profile_counter \
        | sort -t":" -k2