diff options
| author | Théo Zimmermann | 2020-01-07 22:10:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-07 22:10:39 +0100 |
| commit | d8d5631ed89b645e2bce50203a877ef5b5ab4fab (patch) | |
| tree | 0c88c5826e8bce1ed7345e4d2c80319a70dd96dd /dev | |
| parent | cfc41cb79e2364f19d97e7e5c94262132972b0b2 (diff) | |
[merge script] Never bypass outdated branch sanity check.
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..a888998ebf 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -137,7 +137,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi |