Thu, 13 Sep 2012 16:01:42 +0200 | wenzelm | more efficient painting based on cached result; | changeset | files |
Thu, 13 Sep 2012 11:13:00 +0200 | wenzelm | more standard init_components -- particularly important to pick up correct jdk/scala version; | changeset | files |
Thu, 13 Sep 2012 10:28:48 +0200 | nipkow | tuned | changeset | files |
Wed, 12 Sep 2012 23:38:12 +0200 | wenzelm | merged | changeset | files |