| Sun, 04 Sep 2011 16:37:22 +0200 | wenzelm | updated READMEs; | changeset | files |
| Sun, 04 Sep 2011 15:49:59 +0200 | wenzelm | property "tooltip-dismiss-delay" is edited in ms, not seconds; | changeset | files |
| Sun, 04 Sep 2011 15:21:50 +0200 | wenzelm | moved XML/YXML to src/Pure/PIDE; | changeset | files |