You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Sep 11, 2024. It is now read-only.
Context: `fetchdep.sh` attempts to check out a github repository based on the
details in a pull request. To do this, it needs to know how to find the pull
request. So, the github workflows attempt to set environment variables to tell
it. Unfortunately, they currently disagree about what the names of the
environment variables should be.
This appears to have been introduced by #8498.
To simplify matters, we may as well have the script use `${GITHUB_REPOSITORY}`
directly, and remove te unused `REPOSITORY` env var from the workflows.
0 commit comments