| Wed, 09 Apr 2014 17:29:37 +0200 | wenzelm | tuned comments (see Scala version); | changeset | files |
| Wed, 09 Apr 2014 16:22:06 +0200 | wenzelm | dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection; | changeset | files |
| Wed, 09 Apr 2014 15:19:22 +0200 | wenzelm | clarifed results range; | changeset | files |