| Wed, 14 Oct 2015 15:06:42 +0200 | wenzelm | more symbols; | changeset | files |
| Wed, 14 Oct 2015 14:21:00 +0200 | wenzelm | clarified control symbols; | changeset | files |
| Wed, 14 Oct 2015 14:15:13 +0200 | wenzelm | added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono; | changeset | files |
| Tue, 13 Oct 2015 21:27:30 +0200 | wenzelm | tuned signature (cf. XML.trim_blanks); | changeset | files |
| Tue, 13 Oct 2015 20:58:59 +0200 | wenzelm | added split_lines; | changeset | files |
| Sat, 17 Oct 2015 13:18:43 +0200 | haftmann | qualify some names stemming from internal bootstrap constructions | changeset | files |