Perhaps rather than futzing with the comment it's easier to just change it to something like 'report_metrics' now.
If you're not going to do that I would make the comment something like
# Although this is called report_times, we're abusing it slightly to report non-time but similarly structured data.
If this is not run automatically (is it?) you should add something about it to readme.
« Back to merge proposal
Perhaps rather than futzing with the comment it's easier to just change it to something like 'report_metrics' now.
If you're not going to do that I would make the comment something like
# Although this is called report_times, we're abusing it slightly to report non-time but similarly structured data.
If this is not run automatically (is it?) you should add something about it to readme.