diff options
author | David Lechner <david@pybricks.com> | 2023-01-13 11:07:47 -0600 |
---|---|---|
committer | Damien George <damien.p.george@gmail.com> | 2023-01-16 12:06:17 +1100 |
commit | 4eefe78e8ed409641f30ad6c0edca8ca07a8e934 (patch) | |
tree | bc056a645de3b75a189d518cd4e721fd02a0f318 | |
parent | d02f089058b9623ea976fbeead9b8acbf4d44bc6 (diff) |
github/workflows/code_size: Print code size change.
The intention of using `tee` is to both print the code size change in
the CI logs and save them to a file. Using redirection to a file
caused it to not print the changes.
Signed-off-by: David Lechner <david@pybricks.com>
-rw-r--r-- | .github/workflows/code_size.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/workflows/code_size.yml b/.github/workflows/code_size.yml index de75bfe08..5d955703b 100644 --- a/.github/workflows/code_size.yml +++ b/.github/workflows/code_size.yml @@ -28,7 +28,7 @@ jobs: - name: Build run: source tools/ci.sh && ci_code_size_build - name: Compute code size difference - run: tools/metrics.py diff ~/size0 ~/size1 | tee > diff + run: tools/metrics.py diff ~/size0 ~/size1 | tee diff - name: Save PR number if: github.event_name == 'pull_request' env: |