On Fri, Nov 24, 2023 at 10:07:30PM +0100, Patrice Dumas wrote:
> Hello,
>
> The extra_integer associated type is used for extra information in
> Texinfo tree elements in C that correspond to integers. Currently the
> associated type is long, but in most cases, it is used as an int. I
> think
Hello,
The extra_integer associated type is used for extra information in
Texinfo tree elements in C that correspond to integers. Currently the
associated type is long, but in most cases, it is used as an int. I
think that it should be homogeneous, both storage and use should use the
same type.