From 0f51c426d3f7527390d57544365e1b8c20237878 Mon Sep 17 00:00:00 2001
From: Laurent Rineau <laurent.rineau@cgal.org>
Date: Wed, 1 Jul 2020 16:37:32 +0200
Subject: [PATCH] Add a new script that helps dealing with `integration`

---
 Scripts/developer_scripts/merge_pr_with_label | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100755 Scripts/developer_scripts/merge_pr_with_label

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