diff options
| author | Clement Tsang <34804052+ClementTsang@users.noreply.github.com> | 2021-06-23 23:34:39 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-23 23:34:39 -0400 |
| commit | b67c928f2b889aaf6ab5bab81eb57f1649ef56ca (patch) | |
| tree | df815055cd69bd72660c2ae1e8e96ddecaa6fd8d /docs | |
| parent | 93b899e7458bda4b53a8f3edbb84f4591afaefae (diff) | |
docs: Switch to mike for versioning (#521)
Switches to mike to add versioning to docs.
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/content/contribution/documentation.md | 2 | ||||
| -rw-r--r-- | docs/mkdocs.yml | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/docs/content/contribution/documentation.md b/docs/content/contribution/documentation.md index 88fab072..b7e57d6f 100644 --- a/docs/content/contribution/documentation.md +++ b/docs/content/contribution/documentation.md @@ -26,4 +26,6 @@ There are a few areas where documentation changes are often needed: - For changes to the extended documentation, you'll want [MkDocs](https://www.mkdocs.org/), [Material for MkDocs](https://squidfunk.github.io/mkdocs-material/), and `mdx_truly_sane_lists` installed to provide live reloading and preview for your changes. You can do so through `pip` or your system's package managers. While you don't _need_ these, it'll probably help in making and validating changes. + You may also want [Mike](https://github.com/jimporter/mike), but it isn't really needed. + 3. Once you have your documentation changes done, submit it as a pull request. For more information regarding that, refer to [Issues and Pull Requests](http://127.0.0.1:8000/contribution/issues-and-pull-requests/). diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index addf8479..6780a91f 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -103,10 +103,10 @@ markdown_extensions: - mdx_truly_sane_lists # See https://github.com/mkdocs/mkdocs/issues/545#issuecomment-522196661 extra: -# Versioning -# version: -# provider: mike -# default: nightly + # Versioning + version: + provider: mike + default: nightly # GA analytics: provider: google |