diff --git a/.github/workflows/code_size.yml b/.github/workflows/code_size.yml index 34bdf744cb..f82d1d0c73 100644 --- a/.github/workflows/code_size.yml +++ b/.github/workflows/code_size.yml @@ -33,7 +33,7 @@ jobs: - name: Build run: tools/ci.sh code_size_build - name: Compute code size difference - run: tools/metrics.py diff ~/size0 ~/size1 | tee diff + run: source tools/ci.sh && ci_code_size_report - name: Save PR number if: github.event_name == 'pull_request' env: diff --git a/tools/ci.sh b/tools/ci.sh index 64c9d465d8..17044edf28 100755 --- a/tools/ci.sh +++ b/tools/ci.sh @@ -122,6 +122,11 @@ function ci_code_size_build { return $STATUS } +function ci_code_size_report { + # Allow errors from tools/metrics.py to propagate out of the pipe above. + (set -o pipefail; tools/metrics.py diff ~/size0 ~/size1 | tee diff) +} + ######################################################################################## # .mpy file format