-
Notifications
You must be signed in to change notification settings - Fork 77
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Update the MPS Manual for compatibility with Sphinx 3. #67
Conversation
5078ce1
to
03f5b43
Compare
This also occurs in master at 7fb1ad6 with Sphinx 6.1.3 so there's no reason to think it was introduced by this work. I'm able to remove the layout problem by installing Sphinx 4, so let's specify Sphinx < 5 and make a separate issue for the problem. |
…ntly broken under Sphinx 5 and 6 <#121>. Because that means we're using a variant of Sphinx, also making a venv-installed Sphinx the default.
Just for the record, I tried |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These changes look good.
I did the following steps:
- Checked I could build the manual locally (results and changes are in the pull request thread Update the MPS Manual for compatibility with Sphinx 3. #67 ).
- Read the diffs, focussing on multi-line diffs, but sampling others at random.
- Sampled pages of the built manual that changed at random and checked them against the diffs.
- Checked manual/html/design/protocol.html because it could be affected by a mistake in the new doc code. It wasn't.
- Read the new paragraphs of manual/html/design/doc.html relating to these changes to make sure they explained the new convention. They did.
I created #121 and #122 as a result of this review but they are not issues with this work.
…iew of GitHub pull request 67 <#67>.
Executing pull request merge procedure. Checklist results: |
No description provided.