diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/create_overlays.sh | 2 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 5 |
2 files changed, 3 insertions, 4 deletions
diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index 314ac07e68..41392be5d7 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -75,4 +75,4 @@ done # End the file; copy to overlays folder. echo "fi" >> $OVERLAY_FILE PR_NUMBER=$(printf '%05d' "$PR_NUMBER") -mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-$OVERLAY_BRANCH.sh +mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-${OVERLAY_BRANCH///}.sh 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 |