Fri, 05 Aug 2016 20:45:58 +0200 | wenzelm | tuned -- maxidx unused; | changeset | files |
Fri, 05 Aug 2016 20:26:13 +0200 | wenzelm | tuned; | changeset | files |
Fri, 05 Aug 2016 20:17:27 +0200 | wenzelm | tuned; | changeset | files |
Fri, 05 Aug 2016 18:14:34 +0200 | wenzelm | merged | changeset | files |
Fri, 05 Aug 2016 18:14:28 +0200 | wenzelm | misc tuning and modernization; | changeset | files |
Fri, 05 Aug 2016 16:36:03 +0200 | wenzelm | tuned whitespace; | changeset | files |