| Fri, 05 Jul 2024 13:36:49 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 05 Jul 2024 13:04:39 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 05 Jul 2024 12:53:45 +0200 | wenzelm | clarified signature; | changeset | files |
| 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 |