This repository was archived by the owner on Feb 16, 2023. It is now read-only.
File tree 1 file changed +6
-21
lines changed
1 file changed +6
-21
lines changed Original file line number Diff line number Diff line change 1
- # Reference https://mybinder.readthedocs.io/en/latest/howto/gh-actions-badges.html
2
1
name : Binder Badge
3
2
on :
4
3
pull_request_target :
5
4
types : [opened]
6
5
7
- permissions :
8
- pull-requests :
9
- write
10
-
11
6
jobs :
12
7
binder :
13
8
runs-on : ubuntu-latest
9
+ permissions :
10
+ pull-requests : write
14
11
steps :
15
- - name : comment on PR with Binder link
16
- uses : actions/github-script@v3
17
- with :
18
- github-token : ${{secrets.GITHUB_TOKEN}}
19
- script : |
20
- var PR_HEAD_USERREPO = process.env.PR_HEAD_USERREPO;
21
- var PR_HEAD_REF = process.env.PR_HEAD_REF;
22
- github.issues.createComment({
23
- issue_number: context.issue.number,
24
- owner: context.repo.owner,
25
- repo: context.repo.repo,
26
- body: `[](https://mybinder.org/v2/gh/${PR_HEAD_USERREPO}/${PR_HEAD_REF}?urlpath=retro/tree) :point_left: Launch RetroLab on Binder`
27
- })
28
- env :
29
- PR_HEAD_REF : ${{ github.event.pull_request.head.ref }}
30
- PR_HEAD_USERREPO : ${{ github.event.pull_request.head.repo.full_name }}
12
+ - uses : jupyterlab/maintainer-tools/.github/actions/binder-link@v1
13
+ with :
14
+ github_token : ${{ secrets.github_token }}
15
+ url_path : retro
You can’t perform that action at this time.
0 commit comments