Skip to content

Adomani/periodic reports dev custom action #90

Adomani/periodic reports dev custom action

Adomani/periodic reports dev custom action #90

name: Add comment
on:
pull_request:
types:
- labeled
jobs:
add-comment:
if: github.event.label.name == 'test-ci'
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
- name: Checkout master branch
uses: adomani/get_mathlib4_with_cache@v1
- id: mathlib_stats
run: |
git checkout origin/adomani/periodic_reports_dev_custom_action scripts/mathlib_stats.sh scripts/count_decls.lean
printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)" >> "$GITHUB_OUTPUT"
printf '%s\n' "$(./scripts/mathlib_stats.sh)"
- name: Add comment
run: gh pr comment "$NUMBER" --body "$BODY"
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
GH_REPO: ${{ github.repository }}
NUMBER: ${{ github.event.pull_request.number }}
BODY: ${{ steps.mathlib_stats.outputs.summary }}