Use the GITHUB_TOKEN also for the public https://api.github.com
accesses. Over some networks like public hotspots github is blocking
unauthenticated access.
Signed-off-by: Hauke Mehrtens <hauke@hauke-m.de>
exit 2
fi
-if ! PR_INFO="$(curl -f -s "https://api.github.com/repos/$REPO/pulls/$PRID")"; then
+if [ -n "$GITHUB_TOKEN" ]; then
+ CURL_CMD=" --user \"$GITHUB_TOKEN:x-oauth-basic\" "
+else
+ CURL_CMD=" "
+fi
+
+if ! PR_INFO="$(curl $CURL_CMD -f -s "https://api.github.com/repos/$REPO/pulls/$PRID")"; then
echo "Failed fetch PR #$PRID info" >&2
exit 3
fi