| Wed, 21 May 2014 16:46:14 +0200 | wenzelm | merged | changeset | files |
| Wed, 21 May 2014 16:21:11 +0200 | wenzelm | more uniform Font_Info.Zoom_Box; | changeset | files |
| Wed, 21 May 2014 15:24:42 +0200 | wenzelm | added zoom box, like for outer output windows; | changeset | files |