On Fri, Nov 22, 2019 at 06:11:32AM +0100, Pavel Stehule wrote:> +1
Okay, done. I have added a .gitignore while on it in the path for thefiles generated.--Michael