@@ -51,7 +51,7 @@ if [ "$USE_SSH" = "true" ]; then
5151 # match "github.com" from ssh uri
5252 REPO=${REPO# " ssh://" }
5353 SSH_HOST=$( echo " $REPO " | cut -d " :" -f 1 | cut -d " @" -f 2)
54-
54+
5555 echo " Adding " $SSH_HOST " to known_hosts"
5656
5757 # removes all keys belonging to hostname from a known_hosts file
@@ -66,6 +66,20 @@ cd $WORKING_DIRECTORY
6666git config --global advice.detachedhead false
6767git config --global credential.helper " /bin/sh -c 'echo username=$USERNAME ; echo password=$PASSWORD '"
6868
69+ set +e
70+ git config --global --unset http.proxy
71+ set -e
72+ if [ -n " $HTTP_PROXY " ]; then
73+ echo " Using HTTP_PROXY"
74+ git config --global http.proxy " $HTTP_PROXY "
75+ else
76+ if [ -n " $HTTPS_PROXY " ]; then
77+ echo " Using HTTPS_PROXY"
78+ git config --global http.proxy " $HTTPS_PROXY "
79+ fi
80+ fi
81+
82+
6983if [ -n " $SPARE_CHECKOUT " ]; then
7084 echo " spare checkout"
7185 if [ -d " $CLONE_DIR " ]; then
@@ -76,11 +90,11 @@ if [ -n "$SPARE_CHECKOUT" ]; then
7690 chmod -R 774 $CLONE_DIR
7791 cd $CLONE_DIR
7892 git remote add origin $REPO
79- git config core.sparsecheckout true
80- echo " $SOURCE /*" >> .git/info/sparse-checkout
93+ git config core.sparsecheckout true
94+ echo " $SOURCE /*" >> .git/info/sparse-checkout
8195 fi
82-
83- git pull --depth=1 origin $REVISION
96+
97+ git pull --depth=1 origin $REVISION
8498 exit 0
8599 fi
86100
0 commit comments