Changes to Gentle Introduction to HARK #2665
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #./github/workflows/chatops-binder.yaml | |
| name: Chatops Binder | |
| on: [issue_comment] # issues and PRs are equivalent in terms of comments for the GitHub API | |
| 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') | |
| 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@v6 | |
| with: | |
| github-token: ${{secrets.GITHUB_TOKEN}} | |
| script: | | |
| // Get the branch name | |
| github.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({ | |
| issue_number: context.payload.issue.number, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| body: `[](https://mybinder.org/v2/gh/${context.repo.owner}/${context.repo.repo}/${BRANCH_NAME}) :point_left: Launch a binder notebook on this branch` | |
| }) | |
| }) |