Tue, 19 Nov 2024 15:25:11 +0100 | wenzelm | re-use Output_Area; | changeset | files |
Tue, 19 Nov 2024 10:52:02 +0100 | wenzelm | re-use Output_Area with search results; | changeset | files |
Tue, 19 Nov 2024 10:40:19 +0100 | wenzelm | re-use Output_Area with search results; | changeset | files |
Tue, 19 Nov 2024 10:14:22 +0100 | wenzelm | more thorough init; | changeset | files |
Tue, 19 Nov 2024 10:11:37 +0100 | wenzelm | clarified signature: prefer defaults for Output_Dockable (and its variants); | changeset | files |
Tue, 19 Nov 2024 10:11:17 +0100 | wenzelm | unused; | changeset | files |
Mon, 18 Nov 2024 16:48:11 +0100 | wenzelm | tuned output: formatting is pointless for proportional font; | changeset | files |