Fri, 25 Nov 2016 14:10:33 +0100 | wenzelm | avoid extra space intruding rail diagrams (amending 4854f7ee0987); | changeset | files |
Thu, 24 Nov 2016 15:21:54 +0100 | wenzelm | explicit option editor_generated_input_delay, which is more aggressive by default; | changeset | files |