Alexander Strasser wrote on Thu, 9 Jul 2020 09:04:53 +0200: > I could setup a mirror for e.g. Github. We probably will get error reports and pull requests there then. (I don't know whether this can be disabled.) This could mean extra work. Ingo