diff options
| author | Maxime Dénès | 2018-11-23 13:35:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-23 13:35:22 +0100 |
| commit | 371efb58fd9b528743a79b07998a5287fbc385d2 (patch) | |
| tree | 098bf449becf60eb30c8ade630b309f32e8b4bae | |
| parent | 8fb01564fba587142c2471708ff18219f1c64903 (diff) | |
| parent | adf5ffcce1012e3af591d0227d2ee3dece2d983a (diff) | |
Merge PR #9021: merge-pr: Improve overlay check
| -rwxr-xr-x | dev/tools/merge-pr.sh | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 320ef6ed07..5fd8a3b7d9 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -202,9 +202,8 @@ info "merging" git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e # TODO: improve this check -if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then - warning "this PR may have overlays (sorry the check is not perfect)" - warning "if it has overlays please check the following:" +if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then + warning "this PR has overlays, please check the following:" warning "- each overlay has a corresponding open PR on the upstream repo" warning "- after merging please notify the upstream they can merge the PR" fi |