diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml index 2d2a7372ed..cc237512e6 100644 --- a/tests/bench/speedcenter.exec.yaml +++ b/tests/bench/speedcenter.exec.yaml @@ -23,7 +23,7 @@ bash -c " set -euxo pipefail && echo -n 'lines: ' && - find library -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 + find library -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1" max_runs: 1 runner: output #- attributes: