This adds the new option GITHUB_NO_PUSH which will prevent the script
from doing any changes to remote repositories.
Signed-off-by: Hauke Mehrtens <hauke@hauke-m.de>
exit 9
fi
+ if [ "$GITHUB_NO_PUSH" = "1" ]; then
+ echo "next commands:"
+ if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "true" ]; then
+ echo "$GIT push $PR_USER HEAD:$PR_BRANCH --force"
+ echo "$GIT checkout $BRANCH"
+ echo "$GIT merge --ff-only $PR_USER/$PR_BRANCH"
+ else
+ echo "$GIT checkout $BRANCH"
+ echo "$GIT merge --ff-only $LOCAL_PR_BRANCH"
+ fi
+ echo "$GIT push"
+ echo "$GIT branch -D $LOCAL_PR_BRANCH"
+ exit 20
+ fi
+
echo "Force pushing $LOCAL_PR_BRANCH to HEAD:$PR_BRANCH for $PR_USER"
if ! $GIT push $PR_USER HEAD:$PR_BRANCH --force; then
echo "Failed to force push HEAD to $PR_USER" >&2