diff options
| author | Gaëtan Gilbert | 2018-11-18 15:20:38 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-18 15:20:38 +0100 |
| commit | adf5ffcce1012e3af591d0227d2ee3dece2d983a (patch) | |
| tree | be5fa67c78aa292cc3cf4306222031fcc3d22758 /dev | |
| parent | 25e989019f72bd435d84a1d495c7de25165556dd (diff) | |
merge-pr: Improve overlay check
Diffstat (limited to 'dev')
| -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 |