Automatically place a launch badge on pull requests#
You can facilitate review of GitHub pull requests on mybinder.org by using GitHub Actions to place a badge or link on Pull Requests. Below are several examples of how to accomplish this.
To enable GitHub Actions, you must place .yaml files that define your GitHub Action workflow in the /.github/workflows/
directory in your repository.
Example 1: Comment on pull request with a binder badge#
The below action uses the github/script Action to call the GitHub API for the purposes of making a comment on a PR that looks like this:
👈 Launch a binder notebook on branch xxxxxxx
Download the below file: binder-badge.yaml
#./.github/workflows/binder-badge.yaml
name: Binder Badge
on:
pull_request_target:
types: [opened]
jobs:
binder:
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
- name: comment on PR with Binder link
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.rest.issues.createComment({
issue_number: context.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
body: `[](https://mybinder.org/v2/gh/${PR_HEAD_USERREPO}/${PR_HEAD_REF}) :point_left: Launch a binder notebook on branch _${PR_HEAD_USERREPO}/${PR_HEAD_REF}_`
})
env:
PR_HEAD_REF: ${{ github.event.pull_request.head.ref }}
PR_HEAD_USERREPO: ${{ github.event.pull_request.head.repo.full_name }}
Example 2: Comment with a Binder badge in response to a comment#
In the below example, we will trigger GitHub Actions to run after someone comments on a pull request with the command /binder
, which will trigger Actions to comment on a PR in the same way as Example 1.
Download the below file: chatops-binder.yaml
#./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.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.rest.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`
})
})
Permissions#
You may want to restrict who can trigger a binder badge to be created by their association with a repository. When triggering GitHub Actions on an issue_comment event, you can
access the association of the person who opened the pull request with the variable github.event.issue.author_association
and the person commenting on the pull request with github.event.comment.author_association
.
Note
An issue_comment
event is triggered when you comment on a pull request. This is because the GitHub API treats issues and pull requests as the same entity in many places. This is also why you can access the association of the person who opened the pull request with the github.event.issue.author_association
when the issue_comment
event occurs.
Similarly, when triggering GitHub Actions on a pull_request event, you can access the association of the person who opened the pull request with the variable github.event.pull_request.author_association
.
For example, this is how you can conditionally trigger the workflow shown in Example 1 if the person opening the PR is a OWNER
, COLLABORATOR
, MEMBER
, or CONTRIBUTOR
:
Download the below file: binder-badge-permissions.yaml
#./github/workflows/binder-badge-permissions.yaml
name: Binder Badge
on: [pull_request]
jobs:
binder:
if: |
(
(github.event.issue.author_association == 'OWNER') ||
(github.event.issue.author_association == 'COLLABORATOR') ||
(github.event.issue.author_association == 'CONTRIBUTOR') ||
(github.event.issue.author_association == 'MEMBER')
)
runs-on: ubuntu-latest
permissions:
pull-requests: write
steps:
- name: comment on PR with Binder link
uses: actions/github-script@v6
with:
github-token: ${{secrets.GITHUB_TOKEN}}
script: |
var BRANCH_NAME = process.env.BRANCH_NAME;
github.rest.issues.createComment({
issue_number: context.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`
})
env:
BRANCH_NAME: ${{ github.event.pull_request.head.ref }}
Further Reading#
There are many more ways you can customize your workflows to suit your needs. Please see the official GitHub Actions documentation for more information.