From d05a5bbd2249094450b553f701492661eaa4d33b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Collonval?= <fcollonval@gmail.com>
Date: Thu, 17 Feb 2022 12:56:47 +0100
Subject: [PATCH] Add binder badge on PR

---
 .github/workflows/binder-on-pr.yml | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 .github/workflows/binder-on-pr.yml

diff --git a/.github/workflows/binder-on-pr.yml b/.github/workflows/binder-on-pr.yml
new file mode 100644
index 00000000..06740d10
--- /dev/null
+++ b/.github/workflows/binder-on-pr.yml
@@ -0,0 +1,29 @@
+# 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: `[![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 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 }}