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. -- Enrico
