-
Check the current branch with git branch --show-current. If not on dev, abort.
-
Find the open PR for dev → master:
gh pr list --head dev --base master --state open --json number,title,url
If no open PR exists, abort with an error message.
-
Squash-merge the PR:
gh pr merge NUMBER --squash --delete-branch
This will also delete the remote dev branch.
-
Switch to master and pull:
git checkout master
git pull
-
Delete the local dev branch if it still exists:
git branch -D dev 2>/dev/null || true
-
Report success with the merged PR URL and the new commit on master.