diff options
| author | Jeff Epler <jepler@gmail.com> | 2025-09-03 13:45:41 -0500 |
|---|---|---|
| committer | Damien George <damien@micropython.org> | 2025-10-08 15:08:21 +1100 |
| commit | 77729fe3f7198dc5c6f353ec78856159544c7abf (patch) | |
| tree | 6c70a398d7aea6012e5a13e38e734d0b48e0e27b /tools/metrics.py | |
| parent | fef414eca49c44180fba9a0ab32e647c0373e67f (diff) | |
tools/ci.sh: Manipulate pipefail better.
Signed-off-by: Jeff Epler <jepler@unpythonic.net>
Diffstat (limited to 'tools/metrics.py')
0 files changed, 0 insertions, 0 deletions