wenzelm [Wed, 13 Dec 2023 19:55:50 +0100] rev 79259
tuned signature;
wenzelm [Wed, 13 Dec 2023 15:23:03 +0100] rev 79258
tuned whitespace;
wenzelm [Wed, 13 Dec 2023 14:58:49 +0100] rev 79257
minor performance tuning;
wenzelm [Mon, 11 Dec 2023 22:08:43 +0100] rev 79256
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
wenzelm [Mon, 11 Dec 2023 21:56:24 +0100] rev 79255
merged
wenzelm [Mon, 11 Dec 2023 21:31:58 +0100] rev 79254
minor performance tuning;
wenzelm [Mon, 11 Dec 2023 21:17:28 +0100] rev 79253
tuned;
wenzelm [Mon, 11 Dec 2023 21:09:24 +0100] rev 79252
minor performance tuning: prefer Same.operation;
wenzelm [Mon, 11 Dec 2023 20:53:01 +0100] rev 79251
clarified signature;
minor performance tuning: avoid redundant identity;
wenzelm [Mon, 11 Dec 2023 20:17:13 +0100] rev 79250
minor performance tuning;
wenzelm [Mon, 11 Dec 2023 19:51:30 +0100] rev 79249
more operations;
wenzelm [Mon, 11 Dec 2023 19:36:28 +0100] rev 79248
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];