It seems that sometimes people edit the asciidoc file without rebuilding the corresponding HTML file. I've rebuilt all files; some are only minor changes because of a new asciidoc utility version.
Perhaps a GitHub workflow should be added, either to check that HTML has been rebuilt for PRs, or a semi-regularly scheduled one to send in a PR rebuilding all of these.
It seems that sometimes people edit the asciidoc file without rebuilding the corresponding HTML file. I've rebuilt all files; some are only minor changes because of a new asciidoc utility version.
Perhaps a GitHub workflow should be added, either to check that HTML has been rebuilt for PRs, or a semi-regularly scheduled one to send in a PR rebuilding all of these.