Skip to content

feat(Integral/Pi): a version of polarCoord for pi integrals #62580

feat(Integral/Pi): a version of polarCoord for pi integrals

feat(Integral/Pi): a version of polarCoord for pi integrals #62580

name: Add "ready-to-merge" and "delegated" label from comment
on:
issue_comment:
types: [created]
jobs:
add_ready_to_merge_label:
name: Add ready-to-merge label
if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
runs-on: ubuntu-latest
steps:
- id: user_permission
uses: actions-cool/check-user-permission@v2
with:
require: 'admin'
- if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
uses: octokit/[email protected]
id: add_label
name: Add label
with:
route: POST /repos/:repository/issues/:issue_number/labels
repository: ${{ github.repository }}
issue_number: ${{ github.event.issue.number }}
labels: '["ready-to-merge"]'
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
id: remove_labels
name: Remove "awaiting-author"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
run: |
curl --request DELETE \
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-author \
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
add_delegated_label:
name: Add delegated label
if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
runs-on: ubuntu-latest
steps:
- id: user_permission
uses: actions-cool/check-user-permission@v2
with:
require: 'admin'
- if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
uses: octokit/[email protected]
id: add_label
name: Add label
with:
route: POST /repos/:repository/issues/:issue_number/labels
repository: ${{ github.repository }}
issue_number: ${{ github.event.issue.number }}
labels: '["delegated"]'
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}