Re: (Small) error in Notation Reference

[James]

Hello,

On 15 May 2012 23:35, Trevor Daniels <address@hidden> wrote:
>
> James you wrote Tuesday, May 15, 2012 11:22 PM
>
>
>
>>> [James - would you like to fix this, or shall I?]
>>
>>
>> Already made a patch, was about to reply to Philip when you sent your
>> email.
>>
>> I guess it could be pushed without review?
>
>
> Sure.
>
> I think you should remove this comment too:
>
>       % if they are still too close, add more " " pairs
>       % until the result looks good
>
> It doesn't make any sense - I guess it is left over from an earlier version.

Done, pushed as

committer       James Lowe <address@hidden>     
Tue, 15 May 2012 22:43:29 +0000 (23:43 +0100)
commit  a65e32f0ecbd7b9794a03894162cbe2d2501b934

Thanks Philip.

James