Add GitHub link to the docs sidebar

PiperOrigin-RevId: 573621667 Change-Id: Iac0fe218267dd8691bc503f5c8ea31c62ba216a9
2023-10-15 07:57:37 -07:00
parent a9ee497e33
commit 93d1c3c92e
3 changed files with 20 additions and 17 deletions
@@ -49,9 +49,15 @@ extensions = [
    'sphinx_favicon',
    'sphinx_reredirects',
    'sphinx_toolbox.collapse',
+    'sphinx_toolbox.github',
+    'sphinx_toolbox.sidebar_links',
    'mujoco_include',
 ]

+# GitHub-related options
+github_username = 'google-deepmind'
+github_repository = 'mujoco'
+
 # Bibtex references for sphinxcontrib.bibtex
 bibtex_bibfiles = ['references.bib']