Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
doc: more formatting fixes #7727
Affected core subsystem(s)
Description of change
More or less a continuation of #7637.
Fixes some documentation formatting issues, this time split into separate commits (I can squash them, though).