diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-08 15:03:24 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-09 11:07:58 +0100 |
| commit | 9337cd70e356cc48fed6a74f23643995abdd7587 (patch) | |
| tree | c937ad39c8e9a9d13d51e5ab7410e904df6e47d9 /dev/tools | |
| parent | 15bcba0cb00ef759169d2ef7c3cbc21b57f133d2 (diff) | |
[Backport script] Check .mli files are not changed.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1..e4359f703 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 |