| 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 |
| Tue, 09 May 2017 19:52:39 +0200 | wenzelm | enter deeper into history; | changeset | files |
| Tue, 09 May 2017 13:45:35 +0200 | wenzelm | more Jenkins test results; | changeset | files |
| Tue, 09 May 2017 13:42:48 +0200 | wenzelm | clarified order of output; | changeset | files |