diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index ed25a59e8..54b0ac64f 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -150,6 +150,16 @@ function run_make { echo "make -j${JOBS} V=0 $*" make -j${JOBS} V=0 $* 2>$ERRFILE check_error $? + + for path in "src/manaplus" "src/dyecmd"; do + if [[ -f "$path" ]]; then + stat -c '%s %n' "$path" + strip -o "$path.stripped" "$path" + stat -c '%s %n' "$path.stripped" + else + printf "%s does not exist, no strip & exe size summary\n" "$path" + fi + done } function run_make_check { |