| Mon, 18 Dec 2023 14:35:11 +0100 | wenzelm | tuned whitespace; | changeset | files |
| Mon, 18 Dec 2023 12:57:59 +0100 | wenzelm | minor performance tuning: more concise union; | changeset | files |
| Mon, 18 Dec 2023 12:02:58 +0100 | wenzelm | tuned comments; | changeset | files |