src/Tools/jEdit/src-base/plugin.scala
Mon, 04 Sep 2017 20:55:06 +0200 wenzelm tuned signature -- avoid warning during jEdit startup;
less more (0) -1 tip