more robust (again): allow to deactivate main plugin;
authorwenzelm
Thu, 15 Jul 2021 21:35:31 +0200
changeset 73998 b3f2da6bef51
parent 73997 0f61cd0ce803
child 73999 6b213c0115f5
more robust (again): allow to deactivate main plugin;
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
   }
 }