| Wed, 31 Jan 2018 11:18:36 +0100 | wenzelm | clarified modules; | changeset | files |
| 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 |
| Tue, 30 Jan 2018 22:46:00 +0100 | wenzelm | clarified lines: like split_lines; | changeset | files |
| Tue, 30 Jan 2018 20:36:18 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 30 Jan 2018 20:21:55 +0100 | wenzelm | unused; | changeset | files |
| Tue, 30 Jan 2018 20:20:46 +0100 | wenzelm | tuned; | changeset | files |