immibis
/
colobot
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
colobot/.github/workflows/verify-pr-target.yml

22 lines
1.1 KiB
YAML
Raw Normal View History

Migrate to GitHub Actions This is pretty much a straight port of our Jenkinsfile to GitHub Actions. It could use some modernization in a few places, but it should work for now. Note that I left the Jenkinsfile for now - we'll be using them both until we are sure that the GitHub Actions version is stable.
2020-07-07 12:19:21 +00:00
name: Verify pull request target
Send comment when pull request targets the wrong branch
2021-02-22 10:55:51 +00:00
on: [pull_request_target]
Migrate to GitHub Actions This is pretty much a straight port of our Jenkinsfile to GitHub Actions. It could use some modernization in a few places, but it should work for now. Note that I left the Jenkinsfile for now - we'll be using them both until we are sure that the GitHub Actions version is stable.
2020-07-07 12:19:21 +00:00
jobs:
Display correct PR target branch as success rather than skipped
2020-07-07 16:37:21 +00:00
check_pr_target:
Migrate to GitHub Actions This is pretty much a straight port of our Jenkinsfile to GitHub Actions. It could use some modernization in a few places, but it should work for now. Note that I left the Jenkinsfile for now - we'll be using them both until we are sure that the GitHub Actions version is stable.
2020-07-07 12:19:21 +00:00
runs-on: ubuntu-latest
steps:
Send comment when pull request targets the wrong branch
2021-02-22 10:55:51 +00:00
- 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).
Migrate to GitHub Actions This is pretty much a straight port of our Jenkinsfile to GitHub Actions. It could use some modernization in a few places, but it should work for now. Note that I left the Jenkinsfile for now - we'll be using them both until we are sure that the GitHub Actions version is stable.
2020-07-07 12:19:21 +00:00
- name: Wrong pull request target
Display correct PR target branch as success rather than skipped
2020-07-07 16:37:21 +00:00
if: github.base_ref == 'master'
Send comment when pull request targets the wrong branch
2021-02-22 10:55:51 +00:00
run: echo "This pull request targets the master branch. Please edit the pull request to target dev." && exit 1
Display correct PR target branch as success rather than skipped
2020-07-07 16:37:21 +00:00
- name: Correct pull request target
Send comment when pull request targets the wrong branch
2021-02-22 10:55:51 +00:00
if: github.base_ref != 'master'
Display correct PR target branch as success rather than skipped
2020-07-07 16:37:21 +00:00
run: echo "This pull request targets the correct branch." && exit 0