src/Tools/jEdit/src/font_info.scala
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Wed, 21 May 2014 16:21:11 +0200 wenzelm more uniform Font_Info.Zoom_Box;
Tue, 22 Apr 2014 23:49:15 +0200 wenzelm avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
Sat, 01 Mar 2014 19:55:01 +0100 wenzelm clarified module structure;
Sat, 01 Mar 2014 19:43:35 +0100 wenzelm tuned;
Sat, 01 Mar 2014 19:39:27 +0100 wenzelm tuned signature -- separate module Font_Info;
less more (0) tip