Switch the MPS manual to using the Read the Docs theme, to get search capability.

rptb1 · rptb1 · commit 90efeb60a04d · 2023-02-22T04:44:03.000Z
diff --git a/manual/requirements.pip b/manual/requirements.pip
@@ -2,3 +2,4 @@
 
 # Layout breaks in Sphinx >= 5.  See <https://github.com/Ravenbrook/mps/issues/121>.
 sphinx >= 4, < 5
+sphinx-rtd-theme
diff --git a/manual/source/conf.py b/manual/source/conf.py
@@ -37,7 +37,7 @@
 else:
     project = u'Memory Pool System'
     master_doc = 'index'
-    html_theme = 'mps'
+    html_theme = 'sphinx_rtd_theme'
     html_sidebars = {
         '**': ['localtoc.html', 'relations.html', 'links.html', 'contact.html'],
     }

Original file line number	Diff line number	Diff line change
`@@ -2,3 +2,4 @@`
`2`	`2`
`3`	`3`	`# Layout breaks in Sphinx >= 5. See <https://github.com/Ravenbrook/mps/issues/121>.`
`4`	`4`	`sphinx >= 4, < 5`
	`5`	`+sphinx-rtd-theme`
Original file line number	Diff line number	Diff line change
`@@ -37,7 +37,7 @@`
`37`	`37`	`else:`
`38`	`38`	`project = u'Memory Pool System'`
`39`	`39`	`master_doc = 'index'`
`40`		`- html_theme = 'mps'`
	`40`	`+ html_theme = 'sphinx_rtd_theme'`
`41`	`41`	`html_sidebars = {`
`42`	`42`	`'**': ['localtoc.html', 'relations.html', 'links.html', 'contact.html'],`
`43`	`43`	`}`