binder-on-pr.yml 1.1 KB

12345678910111213141516171819202122232425262728293031
  1. # Reference https://mybinder.readthedocs.io/en/latest/howto/gh-actions-badges.html
  2. name: Binder Badge
  3. on:
  4. pull_request_target:
  5. types: [opened]
  6. permissions:
  7. pull-requests: write
  8. jobs:
  9. binder:
  10. runs-on: ubuntu-latest
  11. steps:
  12. - name: comment on PR with Binder link
  13. uses: actions/github-script@v3
  14. with:
  15. github-token: ${{secrets.GITHUB_TOKEN}}
  16. script: |
  17. var PR_HEAD_USERREPO = process.env.PR_HEAD_USERREPO;
  18. var PR_HEAD_REF = process.env.PR_HEAD_REF;
  19. github.issues.createComment({
  20. issue_number: context.issue.number,
  21. owner: context.repo.owner,
  22. repo: context.repo.repo,
  23. body: `[![Binder](https://mybinder.org/badge_logo.svg)](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}_`
  24. })
  25. env:
  26. PR_HEAD_REF: ${{ github.event.pull_request.head.ref }}
  27. PR_HEAD_USERREPO: ${{ github.event.pull_request.head.repo.full_name }}