From 9c6ff0baacbaa9346d093d0fdbc697ee86a38eb6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 29 Aug 2020 12:56:37 +0200 Subject: [PATCH] chore: certainly this one is the right fix --- tests/bench/speedcenter.exec.velcom.yaml | 2 +- tests/bench/speedcenter.exec.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 5a49fc9f75..a11ee6d1c1 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -11,7 +11,7 @@ run_config: <<: *time cmd: | - bash -c 'bench=$PWD/tests/bench; cd ${BUILD:-../../build/release}/stage0; find lib/lean ! -name libleancpp.a -delete; LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py' + bash -c 'bench=$PWD; cd ${BUILD:-../../build/release}/stage0; find lib/lean ! -name libleancpp.a -delete; LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py' max_runs: 2 parse_output: true # Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird. diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml index 34fc63145b..6e50bcbfce 100644 --- a/tests/bench/speedcenter.exec.yaml +++ b/tests/bench/speedcenter.exec.yaml @@ -10,7 +10,7 @@ run_config: <<: *time cmd: | - bash -c 'bench=$PWD/tests/bench; cd ${BUILD:-../../build/release}/stage0; find lib/lean ! -name libleancpp.a -delete; LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py' + bash -c 'bench=$PWD; cd ${BUILD:-../../build/release}/stage0; find lib/lean ! -name libleancpp.a -delete; LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | $bench/accumulate_profile.py' max_runs: 2 parse_output: true # Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird.