Thu, 22 Nov 2012 14:44:37 +0100 | traytel | made SML/NJ happier | changeset | files |
Thu, 22 Nov 2012 17:11:26 +0100 | wenzelm | pack window before accessing its geometry; | changeset | files |
Thu, 22 Nov 2012 17:01:20 +0100 | wenzelm | always refresh font metrics, to help window size calculation (amending 2585c81d840a); | changeset | files |