| Fri, 05 Jul 2024 11:38:21 +0200 | wenzelm | prefer official UTF-8 decoding (in contrast to 2541de190d92): this is also more efficient (factor 10-20); | changeset | files |
| Fri, 05 Jul 2024 10:55:02 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 05 Jul 2024 00:21:47 +0200 | wenzelm | unused (see also c2f176a38448); | changeset | files |