From f5519f8936b919423e36a1f4f6d72b7a12facbc9 Mon Sep 17 00:00:00 2001 From: krzys-h Date: Mon, 22 Feb 2021 11:55:51 +0100 Subject: [PATCH] Send comment when pull request targets the wrong branch --- .github/workflows/verify-pr-target.yml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/.github/workflows/verify-pr-target.yml b/.github/workflows/verify-pr-target.yml index 09cadb19..c5f388d7 100644 --- a/.github/workflows/verify-pr-target.yml +++ b/.github/workflows/verify-pr-target.yml @@ -1,14 +1,21 @@ name: Verify pull request target -on: [pull_request] +on: [pull_request_target] jobs: check_pr_target: runs-on: ubuntu-latest steps: - - name: Wrong pull request target - run: echo "This pull request targets the master branch. Please edit the pull request to target dev." && exit 1 + - name: Send comment if wrong pull request target if: github.base_ref == 'master' + uses: peter-evans/create-or-update-comment@v1 + with: + issue-number: ${{ github.event.number }} + body: | + Hey! This pull request targets the `master` branch. You should probably target `dev` instead. Make sure to read the [contributing guidelines](https://github.com/colobot/colobot/blob/master/CONTRIBUTING.md#submitting-pull-requests) and [edit the target branch if necessary](https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/changing-the-base-branch-of-a-pull-request). + - name: Wrong pull request target + if: github.base_ref == 'master' + run: echo "This pull request targets the master branch. Please edit the pull request to target dev." && exit 1 - name: Correct pull request target + if: github.base_ref != 'master' run: echo "This pull request targets the correct branch." && exit 0 - if: github.base_ref != 'master' \ No newline at end of file