Description

Unless I got something wrong, these files are useless (empty) and they
are not referenced in our docs. I removed them.

The user-patches.sh script got a better documentation and its suffix
.dist removed.

Type of change

• Improvement (non-breaking change that does improve existing functionality)

Checklist:

• My code follows the style guidelines of this project
• I have performed a self-review of my own code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation (README.md or the documentation under docs/)
• If necessary I have added tests that prove my fix is effective or that my feature works
• New and existing unit tests pass locally with my changes