Sun, 29 Dec 2024 15:49:11 +0100 proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
wenzelm [Sun, 29 Dec 2024 15:49:11 +0100] rev 81692
proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
Sun, 29 Dec 2024 15:39:01 +0100 tuned;
wenzelm [Sun, 29 Dec 2024 15:39:01 +0100] rev 81691
tuned;
Sun, 29 Dec 2024 15:34:28 +0100 unused;
wenzelm [Sun, 29 Dec 2024 15:34:28 +0100] rev 81690
unused;
Sun, 29 Dec 2024 15:15:06 +0100 tuned signature;
wenzelm [Sun, 29 Dec 2024 15:15:06 +0100] rev 81689
tuned signature;
Sun, 29 Dec 2024 15:05:16 +0100 tuned: more uniform;
wenzelm [Sun, 29 Dec 2024 15:05:16 +0100] rev 81688
tuned: more uniform;
Sun, 29 Dec 2024 14:57:13 +0100 tuned: more uniform;
wenzelm [Sun, 29 Dec 2024 14:57:13 +0100] rev 81687
tuned: more uniform;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 tip