src/Tools/jEdit/src/jedit/plugin.scala
Tue, 08 Dec 2009 23:18:07 +0100 wenzelm proper actor wiring for raw process output;
Tue, 08 Dec 2009 21:48:12 +0100 wenzelm added properties_changed event bus;
Tue, 08 Dec 2009 20:13:07 +0100 wenzelm tuned;
Tue, 08 Dec 2009 17:56:53 +0100 wenzelm simplified register_fonts;
Tue, 08 Dec 2009 16:30:20 +0100 wenzelm misc modernization of names;
Tue, 08 Dec 2009 14:49:01 +0100 wenzelm misc rearrangement of files;
less more (0) tip