Thu, 07 Nov 2024 20:02:10 +0100 clarified signature;
wenzelm [Thu, 07 Nov 2024 20:02:10 +0100] rev 81393
clarified signature;
Thu, 07 Nov 2024 16:13:58 +0100 clarified output representation: postpone Pretty.separate;
wenzelm [Thu, 07 Nov 2024 16:13:58 +0100] rev 81392
clarified output representation: postpone Pretty.separate;
Thu, 07 Nov 2024 16:03:53 +0100 tuned;
wenzelm [Thu, 07 Nov 2024 16:03:53 +0100] rev 81391
tuned;
Thu, 07 Nov 2024 15:42:35 +0100 tuned: fewer warnings in IntelliJ IDEA;
wenzelm [Thu, 07 Nov 2024 15:42:35 +0100] rev 81390
tuned: fewer warnings in IntelliJ IDEA;
Thu, 07 Nov 2024 13:30:40 +0100 clarified signature: more accurate types;
wenzelm [Thu, 07 Nov 2024 13:30:40 +0100] rev 81389
clarified signature: more accurate types;
Thu, 07 Nov 2024 13:26:31 +0100 tuned signature: more standard names;
wenzelm [Thu, 07 Nov 2024 13:26:31 +0100] rev 81388
tuned signature: more standard names;
Thu, 07 Nov 2024 13:22:59 +0100 more uniform pretty_text_area.zoom via its zoom_component;
wenzelm [Thu, 07 Nov 2024 13:22:59 +0100] rev 81387
more uniform pretty_text_area.zoom via its zoom_component;
Thu, 07 Nov 2024 12:35:55 +0100 tuned signature;
wenzelm [Thu, 07 Nov 2024 12:35:55 +0100] rev 81386
tuned signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 tip