diff --git a/docs/devbox/guides/plugins/index.mdx b/docs/devbox/guides/plugins/index.mdx index 8f920a7..bec5c6f 100644 --- a/docs/devbox/guides/plugins/index.mdx +++ b/docs/devbox/guides/plugins/index.mdx @@ -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:/?dir=" ] ``` +Branch override: +``` + "include": [ "github://?dir=" ] +``` + +Git Tag Pinning: +``` + "include": [ "github://tags/?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