changeset 35854 | 568917059243 |
parent 35848 | 8a7140ec4c89 |
child 35855 | 69d7fcd91696 |
--- a/tests/run-tests.py Wed Jan 31 11:04:16 2018 -0800 +++ b/tests/run-tests.py Wed Jan 31 23:12:45 2018 -0800 @@ -2019,8 +2019,9 @@ try: with open(os.path.join(outputdir, b'.testtimes-')) as fp: for line in fp: - ts = line.split() - times.append((ts[0], [float(t) for t in ts[1:]])) + m = re.match('(.*?) ([0-9. ]+)', line) + times.append((m.group(1), + [float(t) for t in m.group(2).split()])) except IOError as err: if err.errno != errno.ENOENT: raise