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

[Miguel Ojeda]

On Tue, Jul 18, 2023 at 3:54 PM Carlos Bilbao <carlos.bilbao@xxxxxxx> wrote:
>
> The previous patch works without this, the generated HTML will show in the
> Rust index:
>
>   This documentation does not include rustdoc generated information.

I see, thanks, then it does not matter much. I guess you put it in the
first commit because the docs were moved to the URL the docs talk
about, but it still means we are using a tag that does not yet exist,
so I would have put the "link/URL feature" as a separate commit
(together with the creation of the tag).

Cheers,
Miguel