| Fri, 30 Dec 2016 18:02:27 +0100 | haftmann | dropped slightly outdated comment | changeset | files |
| Fri, 30 Dec 2016 20:43:40 +0100 | wenzelm | merged | changeset | files |
| Fri, 30 Dec 2016 20:36:13 +0100 | wenzelm | manage changes of external files; | changeset | files |
| Fri, 30 Dec 2016 17:45:00 +0100 | wenzelm | more explicit edits -- eliminated Clear; | changeset | files |