Fri, 04 Nov 2022 18:59:54 +0100 | wenzelm | merged | changeset | files |
Fri, 04 Nov 2022 17:35:21 +0100 | wenzelm | tuned (again); | changeset | files |
Fri, 04 Nov 2022 17:17:05 +0100 | wenzelm | prefer strict operation (see also f29056da5903); | changeset | files |