Re: replace with Unicode code point
Stephan Hradek <[email protected]>
| Newsgroups | gmane.editors.jedit.user |
|---|---|
| Message-ID | <[email protected]> |
On 17-11-06 23:50, maxwell wrote: > I suspect there's a way to do this with a "BeanShell snippet", but I > don't know beans about this... I think it'll be: "\u0131\u0304" + _1 ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot -- ----------------------------------------------- jEdit Users' List [email protected] https://lists.sourceforge.net/lists/listinfo/jedit-users