Retry for uploading coverage

1 files changed, 19 insertions, 0 deletions

diff --git a/scripts/retry.sh b/scripts/retry.sh
new file mode 100755
index 000000000..82455169a
--- /dev/null
+++ b/scripts/retry.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+#Taken from https://gist.github.com/sj26/88e1c6584397bb7c13bd11108a579746
+
+retries=$1
+shift
+
+count=0
+until "$@"; do
+    exit=$?
+    count=$(($count + 1))
+    if [[ ${count} -lt ${retries} ]]; then
+      echo "Retry ${count}/${retries} exited ${exit}, retrying in ${count} seconds..."
+      sleep ${count}
+    else
+      echo "Retry ${count}/${retries} exited ${exit}, no more retries left."
+      exit ${exit}
+    fi
+done