diff options
| -rwxr-xr-x | doc/sphinx/conf.py | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 363129872..4c153a190 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -146,6 +146,14 @@ html_theme = 'sphinx_rtd_theme' # documentation. #html_theme_options = {} +html_context = { + 'display_github': True, + 'github_user': 'coq', + 'github_repo': 'coq', + 'github_version': 'master', + 'conf_py_path': '/doc/sphinx/' +} + # Add any paths that contain custom themes here, relative to this directory. import sphinx_rtd_theme html_theme_path = [sphinx_rtd_theme.get_html_theme_path()] |