Skip to content

Private Github plugins #1918

Closed
Closed
@jylamont

Description

@jylamont

What problem are you trying to solve?

Devbox allows you to reference plugins hosted by Github, but from what I can tell they only allow public repos. Our company wants to build a plugin for internal use and mark the repo visibility as private, but we run into an authentication issue when attempting to pull.

What solution would you like?

If the user has GITHUB_TOKEN set in their shell (not devbox.json or devbox shell), then token=$GITHUB_TOKEN is appended as a URL param when resolving the Github-hosted plugin URL. For example:

  • If GITHUB_TOKEN is not set, the URL will be: https://raw.githubusercontent.com/<org>/<repo>/master/<plugin-dir>
  • If GITHUB_TOKEN is set to gh_abcd, the URL will be: https://raw.githubusercontent.com/<org>/<repo>/master/<plugin-dir>?token=gh_abcd

Alternatives you've considered

Currently we pull the repo and reference using the local path. This works but my concerns are:

  1. Team members have to manage cloning and updating the local repo
  2. The local path is dependent on where team member clone the repo to, so it can make our devbox.json files brittle.

Metadata

Metadata

Assignees

No one assigned

    Labels

    featureNew feature or requesttriageIssue needs triage

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions