[github] add comment if rights are insufficient to set milestone

This commit is contained in:
Denis Rouzaud 2020-01-10 08:54:51 +01:00
parent ef750839e3
commit a704341b4a

View File

@ -105,3 +105,16 @@ jobs:
milestone: ${{ steps.compute_milestone.outputs.milestone_number }}
owner: ${{ github.event.pull_request.base.repo.owner.login }}
repo: ${{ github.event.pull_request.base.repo.name }}
# if the PR author could not set the milestone due to missing rights, add a comment
- name: leave comment for milestone
if: failure()
uses: octokit/request-action@v2.x
env:
GITHUB_TOKEN: ${{ steps.token.outputs.token }}
with:
route: POST /repos/:owner/:repo/issues/:pull_number/comments
pull_number: ${{ github.event.pull_request.number }}
body: ${{ format("**Calculated milestone for the PR: {0}**", steps.compute_milestone.outputs.milestone_number) }}
owner: ${{ github.event.pull_request.base.repo.owner.login }}
repo: ${{ github.event.pull_request.base.repo.name }}