Skip to content

Commit

Permalink
Comment checkdiff output on PRs
Browse files Browse the repository at this point in the history
  • Loading branch information
Rangi42 committed Oct 22, 2024
1 parent 4c495c3 commit 0a6d18d
Showing 1 changed file with 14 additions and 1 deletion.
15 changes: 14 additions & 1 deletion .github/workflows/checkdiff.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ on: pull_request

jobs:
checkdiff:
permissions:
pull-requests: write
runs-on: ubuntu-latest
steps:
- name: Set up repo
Expand All @@ -12,6 +14,17 @@ jobs:
git remote add upstream "${{ github.event.pull_request.base.repo.clone_url }}"
git fetch upstream
- name: Checkdiff
id: checkdiff
working-directory: rgbds
run: |
make checkdiff "BASE_REF=${{ github.event.pull_request.base.sha }}" Q= | tee log
make checkdiff "BASE_REF=${{ github.event.pull_request.base.sha }}" | tee log
- name: Comment
uses: actions/github-script@v7
with:
script: |
github.rest.issues.createComment({
issue_number: context.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
body: `**Checkdiff:** <pre><code>${{steps.checkdiff.outputs.response}}</code></pre>`
})

0 comments on commit 0a6d18d

Please sign in to comment.