Tue, 10 Sep 2024 15:35:51 +0200 tuned;
wenzelm [Tue, 10 Sep 2024 15:35:51 +0200] rev 80843
tuned;
Tue, 10 Sep 2024 14:53:04 +0200 clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
wenzelm [Tue, 10 Sep 2024 14:53:04 +0200] rev 80842
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
Tue, 10 Sep 2024 12:34:32 +0200 clarified signature;
wenzelm [Tue, 10 Sep 2024 12:34:32 +0200] rev 80841
clarified signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip