| Fri, 06 Dec 2019 19:56:45 +0100 | wenzelm | merged | changeset | files |
| Fri, 06 Dec 2019 17:05:52 +0100 | wenzelm | suppress record types: not working properly; | changeset | files |
| Fri, 06 Dec 2019 16:22:15 +0100 | wenzelm | removed junk; | changeset | files |
| Fri, 06 Dec 2019 16:13:36 +0100 | wenzelm | discontinued somewhat pointless options; | changeset | files |
| Fri, 06 Dec 2019 16:05:24 +0100 | wenzelm | tuned signature; | changeset | files |
| Fri, 06 Dec 2019 15:53:09 +0100 | wenzelm | clarified signature; | changeset | files |
| Fri, 06 Dec 2019 15:44:55 +0100 | wenzelm | export datatypes; | changeset | files |