src/Tools/jEdit/src-base/plugin.scala
Sun, 20 Aug 2017 14:03:23 +0200 wenzelm separate base plugin for important services that should be always available, despite startup errors of the main plugin;
less more (0) tip