src/Tools/jEdit/src/jedit_main.scala
Wed, 26 Sep 2012 23:30:19 +0200 wenzelm some support for jEdit warmstart;
less more (0) tip