diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-08 20:34:06 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-09 10:17:36 +0200 |
commit | fe3977512f18c269e82765995ee1e9ba5d6e4b43 (patch) | |
tree | f994ef92c144763beff4a891d6b8d1a081370762 /dev/tools | |
parent | ff223fac386ab4d0e622d1dc03d47cff34db3311 (diff) |
Add sanity check in merge script: local branch is up-to-date.
In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
Diffstat (limited to 'dev/tools')
-rwxr-xr-x | dev/tools/merge-pr.sh | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c4ee2aa73..60e3d739c 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -110,6 +110,26 @@ if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then ask_confirmation fi; +# Sanity check: the local branch is up-to-date with upstream + +LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD) +UPSTREAM_COMMIT=$(git rev-parse @{u}) +if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then + + # Is it just that the upstream branch is behind? + # It could just be that we merged other PRs and we didn't push yet + + if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then + warning "Your branch is ahead of ${REMOTE}." + warning "You should see this warning only if you've just merged another PR and did not push yet." + ask_confirmation + else + error "Local branch is not up-to-date with ${REMOTE}." + error "Pull before merging." + ask_confirmation + fi +fi + # Sanity check: CI failed STATUS=$(curl -s "$API/commits/$COMMIT/status") |