# HG changeset patch
# User wenzelm
# Date 1489593532 -3600
# Node ID b381558dc51fcee5de2ef8e262077a03c1ef97a9
# Parent  f994a61376eb814ed620010718ae337613948578
keep PIDE.plugin for the sake of still open dockables etc. -- jEdit exits these *after* the stop operation;

diff -r f994a61376eb -r b381558dc51f 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
   }
 }