equal
deleted
inserted
replaced
2015 # newest. |
2015 # newest. |
2016 |
2016 |
2017 def loadtimes(outputdir): |
2017 def loadtimes(outputdir): |
2018 times = [] |
2018 times = [] |
2019 try: |
2019 try: |
2020 with open(os.path.join(outputdir, b'.testtimes-')) as fp: |
2020 with open(os.path.join(outputdir, b'.testtimes')) as fp: |
2021 for line in fp: |
2021 for line in fp: |
2022 m = re.match('(.*?) ([0-9. ]+)', line) |
2022 m = re.match('(.*?) ([0-9. ]+)', line) |
2023 times.append((m.group(1), |
2023 times.append((m.group(1), |
2024 [float(t) for t in m.group(2).split()])) |
2024 [float(t) for t in m.group(2).split()])) |
2025 except IOError as err: |
2025 except IOError as err: |