-
Notifications
You must be signed in to change notification settings - Fork 331
39 lines (35 loc) · 1.22 KB
/
ml_stats_label.yaml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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 #actions/checkout@v4
#with:
# ## fetch the whole repository, to get the history of the last week
# fetch-depth: 0
# ref: 'master'
#- uses: actions/checkout@v4
# with:
# ## fetch the whole repository, to get the history of the last week
# fetch-depth: 0
# ref: 'master'
- id: mathlib_stats
run: |
git checkout origin/adomani/periodic_reports_dev scripts/mathlib_stats.sh
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 }}