File tree Expand file tree Collapse file tree 1 file changed +37
-0
lines changed
Expand file tree Collapse file tree 1 file changed +37
-0
lines changed Original file line number Diff line number Diff line change 1+ name : Syntax changes reminder
2+
3+ on :
4+ pull_request_target :
5+ types : [opened, synchronize, reopened]
6+ paths :
7+ - ' upstream/ocaml_flambda/base-rev.txt'
8+
9+ jobs :
10+ remind :
11+ runs-on : ubuntu-latest
12+ permissions :
13+ pull-requests : write
14+ steps :
15+ - name : Create PR Comment
16+ env :
17+ GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
18+ run : |
19+ REPO=${{ github.repository }}
20+ PR_NUMBER=${{ github.event.pull_request.number }}
21+ COMMENT="## Compiler Merge Checklist
22+
23+ This PR seems to merge changes from Flambda. Please be sure to follow the below steps:
24+
25+ - [ ] Update the magic numbers
26+ - [ ] Update list of compiler flags to ignore
27+ - [ ] Make Merlin know about new relevant compiler flags
28+
29+ If this PR is not merging changes from Flambda, feel free to ignore this comment"
30+
31+ # Check if comment already exists
32+ if ! gh pr view $PR_NUMBER --json comments -q '.comments[].body' --repo $REPO | grep -q "Compiler Merge Checklist"; then
33+ gh pr comment $PR_NUMBER --body "$COMMENT" --repo $REPO
34+ echo "Comment added successfully."
35+ else
36+ echo "Comment already exists. Skipping."
37+ fi
You can’t perform that action at this time.
0 commit comments