| Tue, 09 May 2017 21:43:46 +0200 | wenzelm | more output; | changeset | files |
| Tue, 09 May 2017 21:27:34 +0200 | wenzelm | clarified; | changeset | files |
| Tue, 09 May 2017 21:25:32 +0200 | wenzelm | tuned output; | changeset | files |
| Tue, 09 May 2017 21:06:11 +0200 | wenzelm | more robust update of generated directory; | changeset | files |
| Tue, 09 May 2017 20:36:34 +0200 | wenzelm | more output; | changeset | files |
| Tue, 09 May 2017 20:02:31 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 09 May 2017 19:57:04 +0200 | wenzelm | obsolete; | changeset | files |