jEdit supports property setting via .props files. Properties that are set in this
way effect all users of an jEdit installation. They can override settings of jars
and in turn they can be overridden by user settings.
I have default task patterns No. 0-8 changed in this way. It works well and the user is able to change the patterns in the usable way. But when the user resets the patterns via tasklist.reset-patterns action, he doesn't get the patterns he has had before he changed them - he gets the patterns from within the tasklist.jar, because these are written into the user's properties file.
Wouldn't it be better on pattern reset to not write any properties but remove all pattern definition from the user's properties file? I think this would do a clean RESET in all cases.
|Submitted||rschwenn - 2009-08-06 - 22:16:35z||Assigned||nobody|