Le 18/03/2017 à 14:59, Enrico Forestieri a écrit :
On Wed, Mar 15, 2017 at 06:12:51PM +0100, Enrico Forestieri wrote:
Apparently, nobody has a preference, so I am going to commit the
second patch, i.e., the one using a zero-width space character.
On second thoughts, I am not sure this is the best choice. I just
verified that this character is not searchable and only previewing
the latex source code can reveal its presence. So, it may be
inadvertently spread into a document by copy/paste.
I think we have to make do with the ugly zero-space inset.
Or special/invisible unicode characters could be made visible by
changing the character before painting.
