diff --git a/Scripts/developer_scripts/merge_pr_with_label b/Scripts/developer_scripts/merge_pr_with_label index 5e19508cbed..20f94200d5e 100755 --- a/Scripts/developer_scripts/merge_pr_with_label +++ b/Scripts/developer_scripts/merge_pr_with_label @@ -2,12 +2,14 @@ : ${GITHUB_HUB:=$(which hub)} +label=${1:-"Under Testing"} + if ! [ -x "${GITHUB_HUB}" ]; then echo 'Needs Github hub: https://github.com/github/hub and Github gh: https://github.com/cli/cli' >&2 exit 1 fi -for pr in `gh pr list --label "Under Testing" | awk '{print $1}'`; do +for pr in `gh pr list --label "$label" | awk '{print $1}'`; do if ! hub merge https://github.com/CGAL/cgal/pull/$pr; then echo $pr; exit 1