Merge branch 'bug/1423_ignore_build_files_in_dist' into develop

This commit is contained in:
Marc Faber
2020-11-17 15:50:25 +01:00