Re: Working on Issue 1135

[Neil Puttock]

On 12 September 2011 13:47, Marc Hohl <address@hidden> wrote:

> I created a new directory, made a git repository from scratch,
> changed the one line and did
>
> make all
> make doc

Hmm, in that case, I'm not sure why it doesn't work.  I assume you
changed the offending line to this:

@funindex \\~a

Cheers,
Neil