Wed, 31 Jan 2018 11:09:05 +0100 | wenzelm | clarified signature; | changeset | files |
Tue, 30 Jan 2018 23:01:38 +0100 | wenzelm | clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area; | changeset | files |