Re: [PATCH v7 2/2] docs: Integrate rustdoc generation into htmldocs

[Miguel Ojeda <miguel.ojeda.sandonis@xxxxxxxxx>]

On Mon, Jul 17, 2023 at 5:17 PM Carlos Bilbao <carlos.bilbao@xxxxxxx> wrote:
>
> +       # Let Sphinx know we will include rustdoc
> +       ALLSPHINXOPTS   +=  -t rustdoc

This is needed in the previous patch, no? I don't know if it fails or
just does not work, but either way, perhaps you can split that from
the first commit to put it last.

> +else
> +       @echo "   Skipping Rust documentation since CONFIG_RUST is not y."
> +endif

Is this printed for everybody? If so, then I think it is a good idea
for the future, but perhaps a bit annoying right for most users right
now.

Cheers,
Miguel