Tue, 19 Nov 2024 10:14:22 +0100 more thorough init;
wenzelm [Tue, 19 Nov 2024 10:14:22 +0100] rev 81487
more thorough init;
Tue, 19 Nov 2024 10:11:37 +0100 clarified signature: prefer defaults for Output_Dockable (and its variants);
wenzelm [Tue, 19 Nov 2024 10:11:37 +0100] rev 81486
clarified signature: prefer defaults for Output_Dockable (and its variants);
Tue, 19 Nov 2024 10:11:17 +0100 unused;
wenzelm [Tue, 19 Nov 2024 10:11:17 +0100] rev 81485
unused;
Mon, 18 Nov 2024 16:48:11 +0100 tuned output: formatting is pointless for proportional font;
wenzelm [Mon, 18 Nov 2024 16:48:11 +0100] rev 81484
tuned output: formatting is pointless for proportional font;
Mon, 18 Nov 2024 15:05:31 +0100 clarified Tree_View.init_model: more uniform;
wenzelm [Mon, 18 Nov 2024 15:05:31 +0100] rev 81483
clarified Tree_View.init_model: more uniform;
Mon, 18 Nov 2024 14:47:17 +0100 more robust update;
wenzelm [Mon, 18 Nov 2024 14:47:17 +0100] rev 81482
more robust update;
Mon, 18 Nov 2024 14:35:48 +0100 handle tree selection;
wenzelm [Mon, 18 Nov 2024 14:35:48 +0100] rev 81481
handle tree selection;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 tip