Re: 2.19.31 Notation Reference glitch

[David Kastrup]

Knut Petersen <address@hidden> writes:

> Am 27.12.2015 um 12:29 schrieb David Kastrup:
>> I think the easier option would be to update our version of
>> texinfo.tex again. The current version supports both characters. 
>
> A full build with texinfo.tex version 2015-12-20.12 succeeded and
> cured the problem.

I'm currently doing a build of my own.  It does not appear like any of
the *.txi files have changed since last time.  And texinfo.tex has
gained a few rather interesting index sorting options.  I have no idea
what kind of makeinfo support is required for that to work with other
backends, however.

-- 
David Kastrup