| Fri, 23 Nov 2018 21:50:50 +0100 | wenzelm | support for build_fonts; | changeset | files |
| Fri, 23 Nov 2018 21:47:35 +0100 | wenzelm | more operations; | changeset | files |
| Fri, 23 Nov 2018 16:43:11 +0100 | wenzelm | clarified font_domain: strict excludes e.g. space character; | changeset | files |