| Mon, 10 Apr 2023 14:59:40 +0200 | wenzelm | performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count"; | changeset | files |
| Mon, 10 Apr 2023 14:13:48 +0200 | wenzelm | NEWS; | changeset | files |
| Mon, 10 Apr 2023 13:43:11 +0200 | wenzelm | performance tuning; | changeset | files |