| Thu, 20 May 2010 16:35:53 +0200 | haftmann | adjusted | changeset | files |
| Thu, 20 May 2010 16:35:52 +0200 | haftmann | turned old-style mem into an input abbreviation | changeset | files |
| Thu, 20 May 2010 23:20:01 +0200 | wenzelm | zoom font size; | changeset | files |
| Thu, 20 May 2010 23:19:28 +0200 | wenzelm | added somewhat generic zoom box; | changeset | files |