Wed, 11 Sep 2024 23:26:25 +0200 clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
wenzelm [Wed, 11 Sep 2024 23:26:25 +0200] rev 80866
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
Wed, 11 Sep 2024 23:07:18 +0200 unused;
wenzelm [Wed, 11 Sep 2024 23:07:18 +0200] rev 80865
unused;
Wed, 11 Sep 2024 22:56:42 +0200 misc tuning and clarification (see also 86a31308a8e1);
wenzelm [Wed, 11 Sep 2024 22:56:42 +0200] rev 80864
misc tuning and clarification (see also 86a31308a8e1);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip