You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
# If the merge failed, leave a comment on the PR telling devs how to fix it
68
+
if [[ $MERGED == 0 ]]; then
69
+
gh pr comment --repo $GITHUB_REPOSITORY --body "Merging of this branch with rocm-main has failed and must be resolved by a dev. In your local repo, please run git fetch origin; git checkout $SYNC_BRANCH_NAME; git merge rocm-main` and then git push origin $SYNC_BRANCH_MAIN once any conflicts have been resolved."
0 commit comments