From f62f47b34a958e437419c97d1bae0e1a65a39861 Mon Sep 17 00:00:00 2001
From: Juan Cruz Viotti <jv@jviotti.com>
Date: Fri, 9 Feb 2024 17:48:24 -0400
Subject: [PATCH] Remove unused scripts directory (#735)

Signed-off-by: Juan Cruz Viotti <jv@jviotti.com>
---
 scripts/retry.sh | 23 -----------------------
 1 file changed, 23 deletions(-)
 delete mode 100755 scripts/retry.sh

diff --git a/scripts/retry.sh b/scripts/retry.sh
deleted file mode 100755
index eecbe002..00000000
--- a/scripts/retry.sh
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-set -o errexit
-set -o nounset
-
-if [ $# -lt 1 ]
-then
-  echo "Usage: $0 <command...>" 1>&2
-  exit 1
-fi
-
-RETRIES=5
-EXIT_CODE=1
-while [ "$RETRIES" -gt 0 ] && [ "$EXIT_CODE" != "0" ]
-do
-  echo "(pending retries: $RETRIES)" 1>&2
-  "$@" && EXIT_CODE="$?" || EXIT_CODE="$?"
-  RETRIES="$((RETRIES-1))"
-done
-if [ "$EXIT_CODE" != "0" ]
-then
-  exit "$EXIT_CODE"
-fi