Fix miscellaneous issues with the technical documentation #367

Witiko · 2023-11-06T21:59:27Z

Closes #366.

Fix indents before \end{macrocode}

b006987

Witiko added the documentation Related the technical documentation, the user manual, and the README files label Nov 6, 2023

Witiko added this to the 3.3.0 milestone Nov 6, 2023

Witiko added 8 commits November 6, 2023 23:00

Update CHANGES.md

46504d6

Add a missing space in Section 2.3.2.4

74e2041

Consistently indent first paragraphs after headingFour in technical docs

be659d4

Move tail of Section 2.3.2.2 before Section 2.3.2.1 of technical docs

482aae4

Merge Section 2.3.2.2 into Section 2.3.2.5 of technical docs

058d831

Remove the options.cacheDir directory if it is empty after conversion

d225072

Correctly process heading identifiers in technical docs

33a7694

Update CHANGES.md

ebe8a30

Witiko force-pushed the fix/technical-documentation branch from b0ed576 to ebe8a30 Compare November 6, 2023 23:30

Witiko added 4 commits November 7, 2023 19:08

Fix \begin{markdown} terminated by \markdownEnd in technical docs

5cc9d04

Add a missing \fi after \iffalse in technical docs

049b8e2

Doubly-escape \, in CommonMark text

1cf7944

Add a missing \par after headingFour in technical docs

afe9022

Witiko added the automerge This pull request will be automatically merged after continuous integration has succeeded label Nov 7, 2023

github-actions bot merged commit 00e4a56 into main Nov 7, 2023
12 checks passed

Witiko deleted the fix/technical-documentation branch November 7, 2023 20:57

Witiko modified the milestones: 3.3.0, 3.2.1 Nov 23, 2023

Provide feedback