File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 1010 publish_benchmarks :
1111 runs-on : ubuntu-latest
1212 environment : benchmark
13+ if : ${{ github.event.workflow_run.conclusion == 'success' }}
1314
1415 permissions :
1516 pull-requests : write
4344 jq -s 'add' General.json Misc.json > results.json
4445 env :
4546 GH_TOKEN : ${{ secrets.GITHUB_TOKEN }}
47+ - name : Find PR Number
48+ id : find_pr
49+ run : |
50+ gh pr list --repo ${{ github.repository }} --head ${{ github.event.workflow_run.head_branch}} --json number -q '.[0].number'
51+ echo "pr_number=$PR" >> $GITHUB_OUTPUT
52+ env :
53+ GH_TOKEN : ${{ secrets.GITHUB_TOKEN }}
4654 - name : Comment benchmark results to PR
4755 if : github.event.workflow_run.event == 'pull_request'
4856 uses : hermit-os/github-action-benchmark@main
5462 gh-repository : github.com/CarlWachter/hermit-bench
5563 comment-always : true
5664 ref : ${{ github.event.workflow_run.head_sha }}
57- pr-number : ${{ github.event.workflow_run.pull_requests[0].number }}
65+ pr-number : ${{ steps.find_pr.outputs.pr_number }}
5866 - name : Publish benchmark results to hermit-bench
5967 if : github.event.workflow_run.event == 'push'
6068 uses : hermit-os/github-action-benchmark@main
You can’t perform that action at this time.
0 commit comments