Right now we do this
# construct GitHub URL for pushing
REMOTE="https://$GITHUB_USER:$TOKEN@github.com/$REPO"
# Make sure the branch is on the server
notice "Pushing your branch to GitHub"
git push "$REMOTE" "$BRANCH"
This was handy in the past, but GitHub is introducing fine grained permission tokens, which apparently don't support this. It would be good to support these too
Right now we do this
This was handy in the past, but GitHub is introducing fine grained permission tokens, which apparently don't support this. It would be good to support these too