Thu, 03 Nov 2016 08:10:56 +0100 | nipkow | tuned | changeset | files |
Wed, 02 Nov 2016 11:06:40 +0100 | wenzelm | more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer'); | changeset | files |
Tue, 01 Nov 2016 21:07:13 +0100 | wenzelm | extra newline as for other tools; | changeset | files |