# HG changeset patch
# User wenzelm
# Date 1260299587 -3600
# Node ID 581e919c8730969a523b5b211dc3a380d2070cdf
# Parent  eb0f4a9ec0528c6af627aec048feb942057ef68f
tuned;

diff -r eb0f4a9ec052 -r 581e919c8730 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 18:00:05 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 20:13:07 2009 +0100
@@ -111,7 +111,7 @@
   private def uninstall(view: View) =
     mapping.removeKey(view.getBuffer).get.deactivate
 
-  def switch_active (view: View) =
+  def switch_active(view: View) =
     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
     else install(view)