From 074628806d6b2ec3304d60ab5cfba1c326f67730 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Krassowski?= <5832902+krassowski@users.noreply.github.com> Date: Thu, 11 Apr 2024 16:14:10 +0100 Subject: [PATCH] Link to GitHub repo from the docs (#1415) Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com> --- docs/source/conf.py | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 7da4ade09a..f23398804d 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -150,7 +150,25 @@ # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the # documentation. -html_theme_options = {"navigation_with_keys": False} +html_theme_options = { + "icon_links": [ + { + "name": "GitHub", + "url": "https://github.com/jupyter-server/jupyter_server", + "icon": "fab fa-github-square", + } + ], + "navigation_with_keys": False, + "use_edit_page_button": True, +} + +# Output for github to be used in links +html_context = { + "github_user": "jupyter-server", # Username + "github_repo": "jupyter_server", # Repo name + "github_version": "main", # Version + "doc_path": "docs/source/", # Path in the checkout to the docs root +} # Add any paths that contain custom themes here, relative to this directory. # html_theme_path = []