--- a/src/Tools/jEdit/etc/options Mon Sep 09 15:53:02 2013 +0200
+++ b/src/Tools/jEdit/etc/options Mon Sep 09 16:15:48 2013 +0200
@@ -27,8 +27,11 @@
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-public option jedit_mac_adapter : bool = true
- -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
+public option jedit_macos_application : bool = true
+ -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
+
+public option jedit_macos_preferences : bool = false
+ -- "native Mac OS X preferences menu"
public option jedit_timing_threshold : real = 0.1
-- "default threshold for timing display"