> On 12 Jul 2020, at 08:19, Akim Demaille <[email protected]> wrote: > >> Unfortunately the literal `→` is output as `↦`. So we need to use >> @arrow. > > As a matter of fact, @arrow works in PDF, but not with makeinfo. So > I install this.
TeXinfo Unicode support is dismal, so for systematic use, one will have to use something else.
