Sun, 30 Sep 2018 12:40:57 +0200 | wenzelm | tuned spelling; | changeset | files |
Sun, 30 Sep 2018 12:36:31 +0200 | wenzelm | tuned whitespace and sections; | changeset | files |
Sun, 30 Sep 2018 12:33:42 +0200 | wenzelm | tuned -- eliminated clone; | changeset | files |