12345678910111213141516171819202122232425262728293031 |
- # Reference https://mybinder.readthedocs.io/en/latest/howto/gh-actions-badges.html
- name: Binder Badge
- on:
- pull_request_target:
- types: [opened]
- permissions:
- pull-requests: write
- jobs:
- binder:
- runs-on: ubuntu-latest
- steps:
- - name: comment on PR with Binder link
- uses: actions/github-script@v3
- 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({
- 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}?urlpath=lab) :point_left: Launch a Binder 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 }}
|