tests/run-tests.py
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