Am 03.07.2018 um 17:22 schrieb Riccardo (Jack) Lucchetti:
On Tue, 3 Jul 2018, Sven Schreiber wrote:
> I'm not currently at a machine where the git access is set up, so
> pushing this to git would have to wait until tonight (unless Jack
> does it first).
Done; I also bumped up the version number.
Thanks!
-sven