diff options
Diffstat (limited to 'scripts/create-pull-request')
-rwxr-xr-x | scripts/create-pull-request | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/create-pull-request b/scripts/create-pull-request index e82858bc98..7c6b96d5c4 100755 --- a/scripts/create-pull-request +++ b/scripts/create-pull-request @@ -183,6 +183,7 @@ if [ -n "$WEB_URL" ]; then git push $REMOTE $L_BRANCH:$BRANCH echo "" fi + echo $WEB_URL wget --no-check-certificate -q $WEB_URL -O /dev/null if [ $? -ne 0 ]; then echo "WARNING: Branch '$BRANCH' was not found on the contrib git tree." |