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///g' \ -e 's///g' \ -e 's///g' \ - -e 's/ (.*)//g' \ + -e 's/ (.*)/ /g' \ | grep Profile_counter \ | sort -t":" -k2