diff options
| author | David Eichmann <EichmannD@gmail.com> | 2018-12-19 11:46:13 -0500 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2018-12-21 16:52:38 -0500 |
| commit | 95fbf87886c4a3c076d71d37e1306f64e0e98b57 (patch) | |
| tree | efbdd34dbd519d989f6c7ff828a0be8125cddc55 | |
| parent | 4147df3a83e9dc8ad5015e8d5439de9269f6c20c (diff) | |
| download | haskell-95fbf87886c4a3c076d71d37e1306f64e0e98b57.tar.gz | |
CircleCI: Fix check for git push retry limit.
Test Plan: Observe CircleCI
Reviewers: bgamari
Reviewed By: bgamari
Subscribers: rwbarton, carter
Differential Revision: https://phabricator.haskell.org/D5464
| -rwxr-xr-x | .circleci/push-test-metrics.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.circleci/push-test-metrics.sh b/.circleci/push-test-metrics.sh index d8222b7820..e383a4c4e7 100755 --- a/.circleci/push-test-metrics.sh +++ b/.circleci/push-test-metrics.sh @@ -42,9 +42,9 @@ function reset_append_note_push { # Push the metrics file as a git note. This may fail if another task pushes a note first. In that case # the latest note is fetched and appended. MAX_RETRY=20 -until reset_append_note_push || [ MAX_RETRY = 0 ] +until reset_append_note_push || [ $MAX_RETRY -le 0 ] do ((MAX_RETRY--)) echo "" - echo "Failed to push git notes. Fetching, appending, and retrying..." + echo "Failed to push git notes. Fetching, appending, and retrying... $MAX_RETRY retries left." done |