obsolete;
authorwenzelm
Fri, 11 Oct 2013 22:11:07 +0200
changeset 54326 c5556b404902
parent 54325 2c4155003352
child 54327 148903e47b26
obsolete;
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)