--- a/src/Tools/jEdit/etc/options Thu Sep 26 12:56:59 2013 +0200
+++ b/src/Tools/jEdit/etc/options Thu Sep 26 13:28:26 2013 +0200
@@ -30,12 +30,6 @@
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-option jedit_macos_application : bool = false
- -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
-
-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"