Experimenting with rendering the manual to PDF using rinohtype#270

Draft

rptb1 wants to merge 14 commits intomasterfrom branch/2023-10-22/rinohtype-pdf-manual

+650-584

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 <#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 21, 2023

Breaking up the glossary index with punctuation and spaces, in response to review <#166 (review)>.
rptb1
committed

Commits on Oct 22, 2023

Adding experimental PDF build of manual using rinohtype <https://github.com/brechtm/rinohtype >.
rptb1
committed