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

Merged

rptb1 merged 13 commits into

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
90efeb6
Using the default MPS logo for the manual, to better match the Read the Docs theme colour scheme.
rptb1
committed
17c57ad

Commits on Feb 27, 2023

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

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
1c857ba

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
ebeee66