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 | |
| 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.
| -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 |