diff --git a/Filtered_kernel/developer_scripts/profile_cleanup b/Filtered_kernel/developer_scripts/profile_cleanup index 75bc9fc024f..35b9011ffaa 100755 --- 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///g' \ -e 's///g' \ -e 's/ (.*)/ /g' \ - | grep Profile_counter \ + | grep Profile_branch_counter \ | sort -t":" -k2