| 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 |
| Tue, 01 Nov 2016 19:43:13 +0100 | wenzelm | prefer standard_path for bash arg; | changeset | files |