| Wed, 03 Nov 2010 22:26:53 +0100 | blanchet | standardize on seconds for Nitpick and Sledgehammer timeouts | changeset | files |
| Wed, 03 Nov 2010 20:19:24 +0100 | nipkow | cleaned up | changeset | files |
| Thu, 04 Nov 2010 16:15:13 +0100 | wenzelm | added property "tooltip-margin"; | changeset | files |
| Thu, 04 Nov 2010 10:58:03 +0100 | wenzelm | clarified tooltips: message output by default, extra info via control/command; | changeset | files |
| Thu, 04 Nov 2010 10:33:37 +0100 | wenzelm | warn in correlation with report -- avoid spurious message duplicates; | changeset | files |
| Thu, 04 Nov 2010 10:22:59 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 03 Nov 2010 21:53:56 +0100 | wenzelm | feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu); | changeset | files |