Fri, 17 Jan 2025 19:46:36 +0100 tuned;
wenzelm [Fri, 17 Jan 2025 19:46:36 +0100] rev 81864
tuned;
Fri, 17 Jan 2025 19:40:56 +0100 clarified pattern matching;
wenzelm [Fri, 17 Jan 2025 19:40:56 +0100] rev 81863
clarified pattern matching;
Fri, 17 Jan 2025 19:30:26 +0100 misc tuning;
wenzelm [Fri, 17 Jan 2025 19:30:26 +0100] rev 81862
misc tuning;
Fri, 17 Jan 2025 17:01:43 +0100 misc tuning and clarification;
wenzelm [Fri, 17 Jan 2025 17:01:43 +0100] rev 81861
misc tuning and clarification;
Fri, 17 Jan 2025 16:49:01 +0100 tuned;
wenzelm [Fri, 17 Jan 2025 16:49:01 +0100] rev 81860
tuned;
Fri, 17 Jan 2025 16:22:49 +0100 clarified exceptions and messages: use "error" only for user-errors, not system failures;
wenzelm [Fri, 17 Jan 2025 16:22:49 +0100] rev 81859
clarified exceptions and messages: use "error" only for user-errors, not system failures;
Fri, 17 Jan 2025 16:13:48 +0100 minor performance tuning: more elementary operations;
wenzelm [Fri, 17 Jan 2025 16:13:48 +0100] rev 81858
minor performance tuning: more elementary operations;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 tip