max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: accumulate_profile: accept category names containing digits (e.g. hygiened decl names)

Browse source
This commit is contained in:
Sebastian Ullrich 2023-02-06 13:31:54 +01:00
parent 75252d2b85
commit 3146aa477d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/accumulate_profile.py
View file

@ -6,7 +6,7 @@ import sys
data = sys.stdin.read()
cats = collections.defaultdict(lambda: 0)
for m in re.findall("^([^\n\d]+)([\d.]+)(m?)s$", data, re.MULTILINE):
for m in re.findall("^(.+?) ([\d.]+)(m?)s$", data, re.MULTILINE):
cats[m[0].strip()] += float(m[1]) * (1e-3 if m[2] else 1)
for cat in sorted(cats.keys()):