2021-12-08 11:58:17 -06:00
|
|
|
name: Run when PRs are closed
|
|
|
|
|
on:
|
|
|
|
|
pull_request:
|
|
|
|
|
types:
|
|
|
|
|
- closed
|
2022-02-10 07:01:18 -06:00
|
|
|
concurrency:
|
2022-03-01 04:09:03 -06:00
|
|
|
group: pr-commands-closed-${{ github.event.number }}
|
2021-12-08 11:58:17 -06:00
|
|
|
jobs:
|
|
|
|
|
close_job:
|
|
|
|
|
# this job will only run if the PR has been closed without being merged
|
|
|
|
|
if: github.event.pull_request.merged == false
|
|
|
|
|
runs-on: ubuntu-latest
|
|
|
|
|
steps:
|
|
|
|
|
- run: |
|
|
|
|
|
echo PR #${{ github.event.number }} has been closed without being merged, removing milestone.
|
|
|
|
|
gh pr edit ${{ github.event.number }} --milestone "" --repo $GITHUB_REPOSITORY
|
|
|
|
|
env:
|
|
|
|
|
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
|
