| Fri, 28 May 2010 18:15:22 +0200 | wenzelm | made SML/NJ quite happy; | changeset | files |
| Fri, 28 May 2010 17:48:18 +0200 | wenzelm | reuse main view.font from jEdit; | changeset | files |
| Fri, 28 May 2010 16:01:25 +0200 | wenzelm | deleted some old fonts; | changeset | files |