src/Tools/jEdit/src/font_info.scala
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Mon, 01 Mar 2021 22:50:00 +0100 wenzelm tuned --- avoid deprecated conversions between certain number type;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Mon, 06 Apr 2020 12:53:45 +0200 wenzelm clarified modules;
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