Skip to content

docs: github plugin usage #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lukefaccin wants to merge 1 commit into
base: main
Choose a base branch
from
Open

docs: github plugin usage #9

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions docs/devbox/guides/plugins/index.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,10 +55,21 @@ Sometimes, you may want to share a plugin across multiple projects or users. In
provide a Github reference to a plugin hosted on Github. To install a github hosted plugin, add the
following to the include section of your devbox.json

Default - `master` branch:
```
"include": [ "github:<org>/<repo>?dir=<plugin-dir>" ]
```

Branch override:
```
"include": [ "github:<org>/<repo>/<branch>?dir=<plugin-dir>" ]
```

Git Tag Pinning:
```
"include": [ "github:<org>/<repo>/tags/<tag-to-pin>?dir=<plugin-dir>" ]
```

Note that Devbox will cache Github plugins for 24 hours. This is to aid performance of
`devbox shell` and similar commands, and avoids downloading the plugin from Github each time. In
extenuating circumstances, you can bypass this cache by setting
Expand Down