Re: [CZT-Users] Problems with certain characters in jEdit

[Petra M. <pe...@cs...>]

Tim Miller wrote:
> Petra, the set_toolkit section defines set minus as the unicode 
> character 005C, while the ZTable in the zcharmap plugin defines it 
> as 2216. The version of the standard that I have specifies it as 
> 005C, but I'm not sure whether my version is still up to date. Any 
> clues?

It got changed from 005C to 2216 in the Technical Corrigenda for Defect
Reports 13568/001..013 (December 2006) so I'd expect CZT to use 2216.
I thought I'd chanaged all characters to the new ones but I must have
missed set minus somehow.  Anyway, it should be fixed now (in the SVN
repository).

Thanks for finding and report this bug, Nelis.

Petra