From 7762efc33439efdaff9c7d949f4cbd53790e1e25 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 24 May 2019 16:22:59 +0200 Subject: [PATCH] chore(tests/playground/report): Lean: rename `GC` to `del` --- tests/playground/report.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/playground/report.py b/tests/playground/report.py index f37e37eb3c..4ad6da830e 100755 --- a/tests/playground/report.py +++ b/tests/playground/report.py @@ -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"),