From ea15e79a89b3a464c9453ec843c6f5711ec5a24c Mon Sep 17 00:00:00 2001
From: Laurent Rineau <laurent.rineau@cgal.org>
Date: Fri, 29 Oct 2021 17:06:12 +0200
Subject: [PATCH] Improve merge_pr_with_label

---
 Scripts/developer_scripts/merge_pr_with_label | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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