src/Tools/jEdit/lib/Tools/jedit
Wed, 08 Jun 2011 20:58:51 +0200 wenzelm build jedit as part of regular startup script (in that case depending on jedit_build component);
less more (0) tip