Thu, 12 Sep 2024 19:52:01 +0200 clarified signature;
wenzelm [Thu, 12 Sep 2024 19:52:01 +0200] rev 80875
clarified signature;
Thu, 12 Sep 2024 19:46:08 +0200 prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;
wenzelm [Thu, 12 Sep 2024 19:46:08 +0200] rev 80874
prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;
Thu, 12 Sep 2024 15:09:07 +0200 clarified signature: more explicit operations;
wenzelm [Thu, 12 Sep 2024 15:09:07 +0200] rev 80873
clarified signature: more explicit operations;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip