Tue, 15 Jul 2025 22:05:06 +0200 merged
wenzelm [Tue, 15 Jul 2025 22:05:06 +0200] rev 82880
merged
Tue, 15 Jul 2025 14:25:30 +0200 more robust, for typical error message prefix/suffix;
wenzelm [Tue, 15 Jul 2025 14:25:30 +0200] rev 82879
more robust, for typical error message prefix/suffix;
Tue, 15 Jul 2025 14:24:21 +0200 tuned messages;
wenzelm [Tue, 15 Jul 2025 14:24:21 +0200] rev 82878
tuned messages;
Tue, 15 Jul 2025 12:45:52 +0200 NEWS;
wenzelm [Tue, 15 Jul 2025 12:45:52 +0200] rev 82877
NEWS;
Tue, 15 Jul 2025 12:40:08 +0200 clarified signature: more uniform;
wenzelm [Tue, 15 Jul 2025 12:40:08 +0200] rev 82876
clarified signature: more uniform;
Tue, 15 Jul 2025 12:37:50 +0200 clarified messages;
wenzelm [Tue, 15 Jul 2025 12:37:50 +0200] rev 82875
clarified messages;
Tue, 15 Jul 2025 11:56:24 +0200 more accurate warning;
wenzelm [Tue, 15 Jul 2025 11:56:24 +0200] rev 82874
more accurate warning;
Tue, 15 Jul 2025 11:26:31 +0200 clarified signature;
wenzelm [Tue, 15 Jul 2025 11:26:31 +0200] rev 82873
clarified signature;
Tue, 15 Jul 2025 11:22:02 +0200 tuned (see also 9e7d1c139569);
wenzelm [Tue, 15 Jul 2025 11:22:02 +0200] rev 82872
tuned (see also 9e7d1c139569);
Tue, 15 Jul 2025 11:11:56 +0200 tuned;
wenzelm [Tue, 15 Jul 2025 11:11:56 +0200] rev 82871
tuned;
Tue, 15 Jul 2025 11:27:59 +0200 clarified signature;
wenzelm [Tue, 15 Jul 2025 11:27:59 +0200] rev 82870
clarified signature;
Tue, 15 Jul 2025 11:04:57 +0200 tuned;
wenzelm [Tue, 15 Jul 2025 11:04:57 +0200] rev 82869
tuned;
Tue, 15 Jul 2025 10:48:45 +0200 explicit "dest" rules: no longer declare [elim_format, elim];
wenzelm [Tue, 15 Jul 2025 10:48:45 +0200] rev 82868
explicit "dest" rules: no longer declare [elim_format, elim];
Mon, 14 Jul 2025 22:58:27 +0200 more accurate declarations;
wenzelm [Mon, 14 Jul 2025 22:58:27 +0200] rev 82867
more accurate declarations;
Mon, 14 Jul 2025 12:23:32 +0200 avoid redundant argument (amending af6f55b15749);
wenzelm [Mon, 14 Jul 2025 12:23:32 +0200] rev 82866
avoid redundant argument (amending af6f55b15749);
(0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 tip