diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-12 09:56:05 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-13 12:45:31 +0100 |
commit | ab6519a2f383b4ccb5a9c23c7e26dac581434d1a (patch) | |
tree | b65bf16d79a0eaf8ad1107b58763bf163e53e709 /doc/sphinx/conf.py | |
parent | 45d2b97681bbb25ddd38ca77de69ff3cc84fe7fe (diff) |
[Sphinx] Add "edit on github"
Diffstat (limited to 'doc/sphinx/conf.py')
-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()] |