[ jEdit-devel ] abbrevs in default encoding ?

[Paul L. <pa...@ac...>]

Dear jEditters,

This is striking me.

I'm trying to define elementary things such as the greek letters per 
name in abbreviations and... it doesn't persist... scratch, scratch... 
It's even manually added there.

Well, in Abbrevs.java (cvs-version, about a week old), I see that the 
Abbrevs file (which is a test file, that's cool) is loaded using new 
FileReader(file) or new InputStreamReader(new FileInputStream(xx))... 
which both mean the platform encoding is taken. That must be the reason 
why my "xi" never comes out as "ξ" !

Is it of use I submit a patch ?

thanks

paul