CircleCI: Fix check for git push retry limit.
authorDavid Eichmann <EichmannD@gmail.com>
Wed, 19 Dec 2018 16:46:13 +0000 (11:46 -0500)
committerBen Gamari <ben@smart-cactus.org>
Fri, 21 Dec 2018 21:52:38 +0000 (16:52 -0500)
Test Plan: Observe CircleCI

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, carter

Differential Revision: https://phabricator.haskell.org/D5464

.circleci/push-test-metrics.sh

index d8222b7..e383a4c 100755 (executable)
@@ -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