Thu, 04 Jul 2024 19:16:12 +0200 tuned comments;
wenzelm [Thu, 04 Jul 2024 19:16:12 +0200] rev 80503
tuned comments;
Fri, 05 Jul 2024 10:38:17 +0200 tuned whitespace;
Fabian Huch <huch@in.tum.de> [Fri, 05 Jul 2024 10:38:17 +0200] rev 80502
tuned whitespace;
Fri, 05 Jul 2024 09:52:56 +0200 use ansi colored diffs;
Fabian Huch <huch@in.tum.de> [Fri, 05 Jul 2024 09:52:56 +0200] rev 80501
use ansi colored diffs;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 tip