File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change 3636 find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
3737 echo -n 'bytes .olean: '
3838 find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
39- echo -n 'bytes .olean.ir: '
40- find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean.ir' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
4139 echo -n 'bytes .olean.server: '
4240 find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
4341 echo -n 'bytes .olean.private: '
4442 find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
43+ echo -n 'bytes .ir: '
44+ find ${BUILD:-build/release}/stage2/lib/lean -name '*.ir' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
4545 echo -n 'lines C: '
4646 find ${BUILD:-build/release}/stage2/lib/temp -name '*.c' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1
4747 echo -n 'lines C++: '
You can’t perform that action at this time.
0 commit comments