Switch the MPS manual to using the Read the Docs theme#166

Merged

rptb1 merged 13 commits intomasterfrom

branch/2023-02-22/manual-rtd-theme

Oct 23, 2023

Commits on Feb 22, 2023

Switch the MPS manual to using the Read the Docs theme, to get search capability.
rptb1
committed
Using the default MPS logo for the manual, to better match the Read the Docs theme colour scheme.
rptb1
committed

Commits on Feb 27, 2023

Improving dependencies so that pip isn't run every time.
rptb1
committed
Switching to the Read the Docs theme fixes layout problems described in GitHub issue #121 <https://github.com/Ravenbrook/mps/issues/121>.
rptb1
committed

Commits on Feb 28, 2023

Commits on Mar 5, 2023

Commits on Oct 11, 2023

Catch-up merge of master into branch/2023-02-22/manual-rtd-theme
rptb1
committed

Commits on Oct 20, 2023

Commits on Oct 21, 2023

Breaking up the glossary index with punctuation and spaces, in response to review <https://github.com/Ravenbrook/mps/pull/166#pullrequestreview-1687977425>.
rptb1
committed