| 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 |
| Tue, 30 Jan 2018 20:12:41 +0100 | wenzelm | simplified: prod_count is always NONE; | changeset | files |
| Tue, 30 Jan 2018 19:59:15 +0100 | wenzelm | tuned; | changeset | files |