# HG changeset patch
# User wenzelm
# Date 1381522267 -7200
# Node ID c5556b404902c34d56662ea52c3fbbaa2241e343
# Parent  2c4155003352be3d9c0990f2ec3f328426418cfd
obsolete;

diff -r 2c4155003352 -r c5556b404902 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Oct 11 20:45:21 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Oct 11 22:11:07 2013 +0200
@@ -228,26 +228,6 @@
   }
 
 
-  /* Mac OS X application hooks */
-
-  def handleQuit(): Boolean =
-  {
-    jEdit.exit(jEdit.getActiveView(), true)
-    false
-  }
-
-  def handlePreferences()
-  {
-    CombinedOptions.combinedOptions(jEdit.getActiveView())
-  }
-
-  def handleAbout(): Boolean =
-  {
-    new AboutDialog(jEdit.getActiveView())
-    true
-  }
-
-
   /* main plugin plumbing */
 
   override def handleMessage(message: EBMessage)