--- a/src/Tools/jEdit/etc/options Wed Sep 25 15:40:34 2013 +0200
+++ b/src/Tools/jEdit/etc/options Wed Sep 25 16:05:40 2013 +0200
@@ -30,10 +30,10 @@
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-public option jedit_macos_application : bool = true
+option jedit_macos_application : bool = false
-- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
-public option jedit_macos_preferences : bool = false
+option jedit_macos_preferences : bool = false
-- "native Mac OS X preferences menu"
public option jedit_timing_threshold : real = 0.1