diff options
Diffstat (limited to '.github/setup_ci.sh')
| -rwxr-xr-x | .github/setup_ci.sh | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/.github/setup_ci.sh b/.github/setup_ci.sh index 044c4d12..e4480e61 100755 --- a/.github/setup_ci.sh +++ b/.github/setup_ci.sh @@ -139,16 +139,29 @@ if [ "yes" = "$INSTALL_FIDO_PPA" ]; then sudo apt-add-repository -y ppa:yubico/stable fi -if [ "x" != "x$PACKAGES" ]; then +tries=3 +while [ ! -z "$PACKAGES" ] && [ "$tries" -gt "0" ]; do case "$PACKAGER" in apt) sudo apt update -qq - sudo apt install -qy $PACKAGES + if sudo apt install -qy $PACKAGES; then + PACKAGES="" + fi ;; setup) - /cygdrive/c/setup.exe -q -P `echo "$PACKAGES" | tr ' ' ,` + if /cygdrive/c/setup.exe -q -P `echo "$PACKAGES" | tr ' ' ,`; then + PACKAGES="" + fi ;; esac + if [ ! -z "$PACKAGES" ]; then + sleep 90 + fi + tries=$(($tries - 1)) +done +if [ ! -z "$PACKAGES" ]; then + echo "Package installation failed." + exit 1 fi if [ "${INSTALL_HARDENED_MALLOC}" = "yes" ]; then |