Merge "Switch on curl retry options for fetching get-pip.py"
diff --git a/tools/install_pip.sh b/tools/install_pip.sh
index d57a687..73d0947 100755
--- a/tools/install_pip.sh
+++ b/tools/install_pip.sh
@@ -43,7 +43,7 @@
 
 function install_get_pip {
     if [[ ! -r $LOCAL_PIP ]]; then
-        curl -o $LOCAL_PIP $PIP_GET_PIP_URL || \
+        curl --retry 6 --retry-delay 5 -o $LOCAL_PIP $PIP_GET_PIP_URL || \
             die $LINENO "Download of get-pip.py failed"
     fi
     sudo -H -E python $LOCAL_PIP