update profile script for change in CGAL

2010-12-29 08:47:09 +00:00 · 2010-12-29 08:47:09 +00:00 · 0607d7650f
parent 5f674516b0
commit 0607d7650f
1 changed files with 1 additions and 1 deletions
--- a/Filtered_kernel/developer_scripts/profile_cleanup
+++ b/Filtered_kernel/developer_scripts/profile_cleanup
@ -46,5 +46,5 @@ cat $@ | sed -e 's/CGAL:://g' \
             -e 's/<EK >//g' \
             -e 's/<IK >//g' \
             -e 's/ (.*)/ /g' \
-       | grep Profile_counter \
+       | grep Profile_branch_counter \
       | sort -t":" -k2