|
(#8154)
* doc: fix hotdoc misuse for dynamically generated content
hotdoc has a native include feature for including files inline. Use this
to generate one file for each dynamically generated code block, and
include that file in Commands.md; see:
https://hotdoc.github.io/syntax-extensions.html#smart-file-inclusion-syntax
This permits us to move back to using the in-tree version of the hotdoc
*.md sources, thus fixing the incorrect inclusion of "builddir/" in the
"Edit on github" links which resulted from using copies as the source.
Fixes #8061
* doc: call the dummy file a "stamp" as it is a better known term
|
