| Thu, 17 Apr 2014 11:13:30 +0200 | wenzelm | proper tooltip_lines for multi-line text; | changeset | files |
| Thu, 17 Apr 2014 10:58:10 +0200 | wenzelm | unused; | changeset | files |
| Thu, 17 Apr 2014 10:54:10 +0200 | wenzelm | capitalize more carefully, e.g. relevant for option "ML_exception_trace"; | changeset | files |
| Wed, 16 Apr 2014 21:51:41 +0200 | haftmann | more simp rules for Fun.swap | changeset | files |
| Wed, 16 Apr 2014 18:28:13 +0200 | wenzelm | updated to jdk-8u5; | changeset | files |
| Wed, 16 Apr 2014 14:16:22 +0200 | wenzelm | avoid ooddity: invoke intended function instead of java.awt.Container.invalidate(); | changeset | files |
| Wed, 16 Apr 2014 13:48:35 +0200 | wenzelm | tuned; | changeset | files |