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

chore: bench C++ lines

Browse source
This commit is contained in:
Sebastian Ullrich 2020-02-07 17:14:27 +01:00
parent 6cbb6c89ca
commit 354439dd43
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,8 @@
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
echo -n 'lines C++: ' &&
find src \( -name '*.h' -o -name '*.cpp' \) -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
"
max_runs: 1
runner: output