Skip to content

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now #317

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now

[Merged by Bors] - chore: address porting note in Archive/Imo/Imo1994Q1 -- linarith works now #317

name: Label New Contributors
on:
pull_request:
types: [opened]
jobs:
label-new-contributor:
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
- name: Get PR author
id: pr-author
run: echo "::set-output name=author::$(jq -r .pull_request.user.login "$GITHUB_EVENT_PATH")"
shell: bash
- name: Check if user is new contributor
id: check-contributor
uses: actions/github-script@v5
with:
script: |
const { owner, repo } = context.repo
const author = "${{ steps.pr-author.outputs.author }}"
const prs = await github.rest.pulls.list({
owner,
repo,
state: "closed",
author
})
return (prs.data.length < 5)
- name: Add label if new contributor
if: steps.check-contributor.outputs.result == 'true'
uses: actions/github-script@v5
with:
script: |
const { owner, repo, number } = context.issue
await github.rest.issues.addLabels({
owner,
repo,
issue_number: number,
labels: ['new-contributor']
})