Re: (Small) error in Notation Reference

[Trevor Daniels]

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.

James