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

chore(tests/playground/report): Lean: rename GC to del

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-24 16:22:59 +02:00
parent 9c31425379
commit 7762efc334
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/playground/report.py
View file

@ -24,7 +24,7 @@ def pp(bench, cat, prop):
CATBAG = {
'.lean': ("Lean [s]", "etime"),
'.gcc.lean': ("Lean+GCC9", "etime"),
'.gc.lean': ("GC [%]", "gc"),
'.gc.lean': ("del [%]", "gc"),
'.lean.perf': ("cache misses [1M/s]", "cache-misses"),
'.hs': ("GHC", "etime"),
'.gc.hs': ("GC [%]", "gc"),