Binder badge: use repo.full_name (#208)

GitHub Actor is the user that opened the PR, but this may not be the same as the owner of the fork.

`pull_request.head.repo.full_name` should be the `owner/reponame` of the PR fork

Author: manics

doc/howto/binder-badge.yaml

@@ -11,15 +11,14 @@ jobs:
       with:
         github-token: ${{secrets.GITHUB_TOKEN}}
         script: |
-          var PR_HEAD_USER = process.env.GITHUB_ACTOR;
-          var PR_HEAD_REPO = process.env.PR_HEAD_REPO;
+          var PR_HEAD_USERREPO = process.env.PR_HEAD_USERREPO;
           var PR_HEAD_SHA = process.env.PR_HEAD_SHA;
           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_USER}/${PR_HEAD_REPO}/${PR_HEAD_SHA}) :point_left: Launch a binder notebook on this branch for commit ${PR_HEAD_SHA}`
+            body: `[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/${PR_HEAD_USERREPO}/${PR_HEAD_SHA}) :point_left: Launch a binder notebook on this branch for commit ${PR_HEAD_SHA}`
           })
       env:
         PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
-        PR_HEAD_REPO: ${{ github.event.pull_request.head.repo.name }}
+        PR_HEAD_USERREPO: ${{ github.event.pull_request.head.repo.full_name }}