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

chore: bench .olean byte size

Browse source
This commit is contained in:
Sebastian Ullrich 2020-02-07 17:09:25 +01:00
parent a897f7e7f3
commit 6cbb6c89ca
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/bench/speedcenter.exec.yaml
View file

@ -23,7 +23,10 @@
bash -c "
set -euxo pipefail &&
echo -n 'lines: ' &&
find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1"
find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
echo -n 'bytes .olean: ' &&
find src -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
"
max_runs: 1
runner: output
- attributes: