# HG changeset patch
# User wenzelm
# Date 1626377731 -7200
# Node ID b3f2da6bef51ffeaa7f8827a50f1a744cf33316b
# Parent  0f61cd0ce803f14579ee3b574be33eba9550d6ae
more robust (again): allow to deactivate main plugin;

diff -r 0f61cd0ce803 -r b3f2da6bef51 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:11:39 2021 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:35:31 2021 +0200
@@ -495,7 +495,5 @@
     session.stop()
     file_watcher.shutdown()
     PIDE.editor.shutdown()
-
-    PIDE._plugin = null
   }
 }