Sun, 07 Apr 2019 21:05:22 +0200 traytel NEWS
Sun, 07 Apr 2019 20:02:15 +0200 traytel merged
Sun, 07 Apr 2019 08:26:57 +0200 traytel bundle for cardinal syntax
Sun, 07 Apr 2019 16:04:08 +0200 wenzelm better accessibility of directory content by typing name prefix;
Sun, 07 Apr 2019 12:44:37 +0200 wenzelm uniform JVM heap options for Isabelle/Scala tools and scalac (again);
Sun, 07 Apr 2019 12:41:52 +0200 wenzelm proper etc/preferences;
Sat, 06 Apr 2019 22:26:38 +0200 wenzelm notes about old Java 8 font rendering for low-quality displays;
Sat, 06 Apr 2019 22:09:41 +0200 wenzelm obsolete -- was mostly about 'export_code';
Sat, 06 Apr 2019 22:05:25 +0200 wenzelm support both hinted and unhinted fonts;
Fri, 05 Apr 2019 23:45:35 +0200 wenzelm option to bypass ttfautohint for experimentation (it can have adverse effects);
Fri, 05 Apr 2019 23:01:20 +0200 wenzelm clarified settings: allow for more Java versions;
Fri, 05 Apr 2019 22:58:29 +0200 wenzelm proper default;
Fri, 05 Apr 2019 21:54:08 +0200 wenzelm clarified;
Fri, 05 Apr 2019 17:05:32 +0200 wenzelm auxiliary operation for common uses of 'compile_generated_files';
Fri, 05 Apr 2019 15:02:55 +0100 paulson merged
(0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 tip