Skip to content

a few developer documentation nits

Tony Finch requested to merge 3199-doc-dev into main

A few little things I spotted when re-reading doc/dev and doc/design.

Closes #3199 (closed)

Merge request reports