keep PIDE.plugin for the sake of still open dockables etc. -- jEdit exits these *after* the stop operation;
authorwenzelm
Wed, 15 Mar 2017 16:58:52 +0100
changeset 65266 b381558dc51f
parent 65265 f994a61376eb
child 65267 7e427dff15dd
keep PIDE.plugin for the sake of still open dockables etc. -- jEdit exits these *after* the stop operation;
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 16:55:37 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 16:58:52 2017 +0100
@@ -458,7 +458,5 @@
     exit_models(JEdit_Lib.jedit_buffers().toList)
     session.stop()
     file_watcher.shutdown()
-
-    PIDE._plugin = null
   }
 }