| Thu, 28 Mar 2013 15:00:27 +0100 | wenzelm | maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; | changeset | files |
| Thu, 28 Mar 2013 14:47:37 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 28 Mar 2013 14:01:56 +0100 | wenzelm | proper default browser info for interactive mode, notably thy_deps; | changeset | files |