Miscellaneous documentation fixes and updates

[msimberg]

See individual commit messages for a description of what has changed.

Fixes #1308.

[codacy-production]

Coverage summary from Codacy

See diff coverage on Codacy

Coverage variation	Diff coverage
✅ +0.06% (target: -1.00%)	✅ ∅ (target: 90.00%)

Coverage variation details

	Coverable lines	Covered lines	Coverage
Common ancestor commit (2f15e1d)	18282	13802	75.50%
Head commit (7ebb1ec)	18282 (+0)	13813 (+11)	75.56% (+0.06%)

Coverage variation is the difference between the coverage for the head and common ancestor commits of the pull request branch: <coverage of head commit> - <coverage of common ancestor commit>

Diff coverage details

	Coverable lines	Covered lines	Diff coverage
Pull request (#1310)	0	0	∅ (not applicable)

Diff coverage is the percentage of lines that are covered by tests out of the coverable lines that the pull request added or modified: <covered lines added or modified>/<coverable lines added or modified> * 100%

See your quality gate settings    Change summary preferences

_{Codacy stopped sending the deprecated coverage status on June 5th, 2024. Learn more}

[msimberg]

Needs #1314 for the ripgrep check for @command vs \command.

[aurianer]

LGTM thanks!