Edit 'docs' branch on github temporarily

Tom-Willemsen · Tom-Willemsen · commit 06aeb4232c48 · 2025-04-22T10:12:44.000+01:00
diff --git a/doc/conf.py b/doc/conf.py
@@ -54,7 +54,7 @@
     "display_github": True,  # Integrate GitHub
     "github_user": "ISISComputingGroup",  # Username
     "github_repo": "ibex_developers_manual",  # Repo name
-    "github_version": "master",  # Version
+    "github_version": "docs",  # Version
     "conf_py_path": "/doc/",  # Path in the checkout to the docs root
 }
 

Original file line number	Diff line number	Diff line change
`@@ -54,7 +54,7 @@`
`54`	`54`	`"display_github": True, # Integrate GitHub`
`55`	`55`	`"github_user": "ISISComputingGroup", # Username`
`56`	`56`	`"github_repo": "ibex_developers_manual", # Repo name`
`57`		`- "github_version": "master", # Version`
	`57`	`+ "github_version": "docs", # Version`
`58`	`58`	`"conf_py_path": "/doc/", # Path in the checkout to the docs root`
`59`	`59`	`}`
`60`	`60`