Wed, 22 Dec 2010 14:44:03 +0100 | wenzelm | merged | changeset | files |
Wed, 22 Dec 2010 09:02:43 +0100 | blanchet | made SML/NJ happy | changeset | files |
Wed, 22 Dec 2010 13:49:06 +0100 | wenzelm | check JVM later, to avoid potential conflict with jEdit splash screen; | changeset | files |