diff -r 5ff12177a067 -r 48072f049838 src/Tools/jEdit/etc/options
--- 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"