src/Tools/jEdit/src/session_build.scala
Thu, 14 Apr 2016 12:08:38 +0200 wenzelm clarified modules;
Mon, 23 Nov 2015 19:51:33 +0100 wenzelm clarified font: GUI defaults might change dynamically;
Sat, 14 Nov 2015 18:37:49 +0100 wenzelm tuned message;
Tue, 03 Nov 2015 13:54:34 +0100 wenzelm clarified modules;
Tue, 27 Oct 2015 23:18:32 +0100 wenzelm no icons here -- not a standalone window;
Wed, 30 Sep 2015 23:54:22 +0200 wenzelm tuned GUI;
Wed, 30 Sep 2015 20:48:59 +0200 wenzelm tuned GUI;
Wed, 30 Sep 2015 14:37:21 +0200 wenzelm tuned message;
Wed, 30 Sep 2015 14:32:26 +0200 wenzelm clarified modules;
less more (0) tip