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

chore(tests/bench/speedcenter.exec.yaml): fix again

Browse source
This commit is contained in:
Sebastian Ullrich 2019-08-16 22:24:22 +02:00
parent f1db7e8041
commit 8cc2f731cd
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/speedcenter.exec.yaml
View file

@ -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: