It requires at least one option argument, and the one that provides
"basic information" about the project is --projectinfo, so let's use
that to demo the command.
Fixes#8182
* 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
Jussi Pakkanen