From 9337cd70e356cc48fed6a74f23643995abdd7587 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 8 Jan 2018 15:03:24 +0100
Subject: [Backport script] Check .mli files are not changed.

---
 dev/tools/backport-pr.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev')

diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index d7acf01f1d..e4359f7038 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -50,6 +50,15 @@ else
 
 fi
 
+if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+    echo
+    read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
+    echo
+    if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+        exit 1
+    fi
+fi
+
 if [[ "${OPTION}" == "--stop-before-merging" ]]; then
     exit 0
 fi
-- 
cgit v1.2.3