On 26 Dec 2023 19:50, Mike Frysinger wrote:
> Wrapping the dir info with @ifnottex means it's included in all other
> outputs like html which makes no sense.  Switch to @direntry which is
> specific for this content and is automatically written to the output
> that makes sense, and omitted from the rest.

ping ...

(and the other doc update patches too)
-mike