Merged requested to merge pspacek/make-manin-on-dist-v9_18 into v9_18
We don't need them in the repo, it's sufficient if we pregenerate them while preparing the tarball. That way we don't have overhead while modifying them but they are still available for installations without Sphinx.
I assume that this will make rebases and cherry-picks across branches easier, with less trial and error churn required in the CI.
It's implemented in the way that we build the manpages only when we either have pregenerated pages available at the configure time or sphinx-build is installed and working.
(cherry picked from commit 91104651)
Backport of MR !6520 (merged)