Skip to content

Commit

Permalink
Merge pull request #274 from fcollonval/patch-1
Browse files Browse the repository at this point in the history
Update github-script action
  • Loading branch information
consideRatio committed Jan 3, 2023
2 parents 87a8f4e + 2ae9c15 commit 262366b
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 9 deletions.
4 changes: 2 additions & 2 deletions doc/howto/binder-badge-permissions.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,12 @@ jobs:
pull-requests: write
steps:
- name: comment on PR with Binder link
uses: actions/github-script@v3
uses: actions/github-script@v6
with:
github-token: ${{secrets.GITHUB_TOKEN}}
script: |
var BRANCH_NAME = process.env.BRANCH_NAME;
github.issues.createComment({
github.rest.issues.createComment({
issue_number: context.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
Expand Down
6 changes: 3 additions & 3 deletions doc/howto/binder-badge.yaml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#./.github/workflows/binder-badge.yaml
name: Binder Badge
on:
on:
pull_request_target:
types: [opened]

Expand All @@ -11,13 +11,13 @@ jobs:
pull-requests: write
steps:
- name: comment on PR with Binder link
uses: actions/github-script@v3
uses: actions/github-script@v6
with:
github-token: ${{secrets.GITHUB_TOKEN}}
script: |
var PR_HEAD_USERREPO = process.env.PR_HEAD_USERREPO;
var PR_HEAD_REF = process.env.PR_HEAD_REF;
github.issues.createComment({
github.rest.issues.createComment({
issue_number: context.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
Expand Down
8 changes: 4 additions & 4 deletions doc/howto/chatops-binder.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -5,27 +5,27 @@ on: [issue_comment] # issues and PRs are equivalent in terms of comments for the
jobs:
trigger-chatops:
# Make sure the comment is on a PR, and contains the command "/binder"
if: (github.event.issue.pull_request != null) && contains(github.event.comment.body, '/binder')
if: (github.event.issue.pull_request != null) && contains(github.event.comment.body, '/binder')
runs-on: ubuntu-latest
steps:
# Use the GitHub API to:
# (1) Get the branch name of the PR that has been commented on with "/binder"
# (2) make a comment on the PR with the binder badge
- name: comment on PR with Binder link
uses: actions/github-script@v3
uses: actions/github-script@v6
with:
github-token: ${{secrets.GITHUB_TOKEN}}
script: |
// Get the branch name
github.pulls.get({
github.rest.pulls.get({
owner: context.repo.owner,
repo: context.repo.repo,
pull_number: context.payload.issue.number
}).then( (pr) => {
// use the branch name to make a comment on the PR with a Binder badge
var BRANCH_NAME = pr.data.head.ref
github.issues.createComment({
github.rest.issues.createComment({
issue_number: context.payload.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
Expand Down

0 comments on commit 262366b

Please sign in to comment.