diff --git a/Scripts/developer_scripts/merge_pr_with_label b/Scripts/developer_scripts/merge_pr_with_label new file mode 100755 index 00000000000..2598ef8c0cc --- /dev/null +++ b/Scripts/developer_scripts/merge_pr_with_label @@ -0,0 +1,15 @@ +#!/bin/bash + +: ${GITHUB_HUB:=$(which hub)} + +if ! [ -x "${GITHUB_HUB}" ]; then + echo 'Needs Github hub: https://github.com/github/hub' >&2 + exit 1 +fi + +for pr in $(python3 ./Scripts/developer_scripts/list_pull_requests.py "$1" --unmerged); do + if ! hub merge $pr; then + echo $p; + break + fi +done