Skip to content

test: length statistics #15

test: length statistics

test: length statistics #15

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:
- uses: actions/checkout@v4
with:
## fetch the whole repository, to get the history of the last week
fetch-depth: 0
#ref: 'master'
- id: print_it
run: |
#git checkout master
## should the next step be removed for Zulip?
#git checkout -
#git checkout adomani/periodic_reports_dev
printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)"
- id: mathlib_stats
run: |
#git checkout adomani/periodic_reports_dev
git checkout -q master
git checkout origin/adomani/periodic_reports_dev scripts/mathlib_stats.sh
## should the next step be removed for Zulip?
#git checkout -q -
printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)"
printf $'summary<<EOF\n%s\nEOF' "$(./scripts/mathlib_stats.sh)" >> "$GITHUB_OUTPUT"
- 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 }}