diff options
| author | Mary <me@thog.eu> | 2021-05-14 11:08:46 +0200 |
|---|---|---|
| committer | Mary <me@thog.eu> | 2021-05-14 11:08:46 +0200 |
| commit | f48828351c759ef63e015ca9806406fab278c458 (patch) | |
| tree | c797b2d3320061e43b59b449fa4d640e1a9f49dd /.github | |
| parent | e318022b89dfd2e7a5db6722eb7663fa9f9bca3c (diff) | |
ci: Do not enforce userid on nightly PR comment
This avoid issues when two different users work on a single PR.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/nightly_pr_comment.yml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/.github/workflows/nightly_pr_comment.yml b/.github/workflows/nightly_pr_comment.yml index c6f7528c..7145b7b6 100644 --- a/.github/workflows/nightly_pr_comment.yml +++ b/.github/workflows/nightly_pr_comment.yml @@ -14,13 +14,12 @@ jobs: const {owner, repo} = context.repo; const run_id = ${{github.event.workflow_run.id}}; const pull_head_sha = '${{github.event.workflow_run.head_sha}}'; - const pull_user_id = ${{github.event.sender.id}}; const issue_number = await (async () => { const pulls = await github.pulls.list({owner, repo}); for await (const {data} of github.paginate.iterator(pulls)) { for (const pull of data) { - if (pull.head.sha === pull_head_sha && pull.user.id === pull_user_id) { + if (pull.head.sha === pull_head_sha) { return pull.number; } } |
