[Sphinx] Add "edit on github"

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()]