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 |