Bruce Richardson, Oct 22, 2024 at 17:25:
No strong objection to this. Just FYI, the reason it is currently done as it is in the build, is that even if you configure a build without the docs enabled, you can just build the docs explicitly by doing "ninja -C build doc". That is so that one can do a test build of the docs without a) having to reconfigure the whole project b) not have every build from then on rebuild e.g. the APIs doc if you change a header.
Oh, I didn't know it was on purpose. I was surprised to see doc related warnings with -Denable_docs=false.
Feel free to disregard this patch if you think it is too drastic.