2020-10-02 20:56:19 +00:00
|
|
|
name: PR merged
|
|
|
|
|
on:
|
2020-10-02 21:09:58 +00:00
|
|
|
pull_request_target:
|
2020-10-09 15:19:13 +00:00
|
|
|
types: [opened, reopened, synchronize, edited, closed]
|
2020-10-02 20:56:19 +00:00
|
|
|
|
|
|
|
|
jobs:
|
|
|
|
|
label-merged:
|
|
|
|
|
name: Changelog needed
|
|
|
|
|
runs-on: ubuntu-latest
|
2020-10-09 15:19:13 +00:00
|
|
|
if: "!(github.event.action == 'closed' && github.event.pull_request.merged == false)"
|
2020-10-02 20:56:19 +00:00
|
|
|
steps:
|
|
|
|
|
- uses: actions/labeler@main
|
|
|
|
|
with:
|
|
|
|
|
repo-token: ${{ secrets.GITHUB_TOKEN }}
|
2020-10-09 15:19:13 +00:00
|
|
|
sync-labels: true
|
