From ab6519a2f383b4ccb5a9c23c7e26dac581434d1a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 12 Mar 2018 09:56:05 +0100 Subject: [Sphinx] Add "edit on github" --- doc/sphinx/conf.py | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'doc') 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()] -- cgit v1.2.3