Re: [ jEdit-devel ] Clear Properties Macro

[Damien R. <dam...@gm...>]

It does make a backup; it saves the properties file to properties.orig. And
it's based on a fixed set; anything defined in the property files that come
with jEdit or in any plugin's property file will be kept. I understand that
it's somewhat risky, but I posted it to jedit-devel with the idea of making
it less so. This was partly in response to your comment in the other
conversation about there not being a way to clear out unused properties, and
so this was my first step in attempting to accomplish that.

Regarding properties defined dynamically, if there is a way to save those in
the plugin's cache then there's no problem, because each plugin's cache is
where the macro searches for properties to keep, not necessarily in the
hard-coded .props file.