Background: we have 2 separate installs of jedit tailored for 2 different workfows (multi-user). Attempting to merge them using '-settings=/some/where/else' command-line switch:
dmaziuk@stingray:~$ java -Xmx96m -Xms24m -jar /share/java/jEdit/5.0.0/jedit.jar -noserver -settings=/share/java/jEdit/mrannotator/
12:56:25 PM [main] [error] main: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/activity.log (Permission denied)
After making that a+w:
PluginJAR: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/jars-cache/QuickNotepad.jar.summary (No such file or directory)
IOUtilities: Error moving file: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/properties (Is a directory) : /share/java/jEdit/mrannotator/properties (Is a directory)
12:57:18 PM [AWT-EventQueue-0] [error] jEdit: Failed to rename "/share/java/jEdit/mrannotator/#properties#save#" to the user properties file "/share/java/jEdit/mrannotator/properties"
So clearly '-settings' overrides "user.home/.jedit" -- why have it in the first place when I can just 'java -Duser.home=/some/place/else' ?
Or should I file a feature request for (e.g.) '-global-settings=' switch instead ?