--- 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
}
}