Add a trivial script to extract the times from *.report.txt files.