Add licensing and copyright information for all files in this repository. This
either happens in the file itself as a comment header or in the file
`.reuse/dep5`.
This commit also adds a Github workflow to check pull requests and adapts
copyright.pl to the changes.
Closes#8869
The wrapper will exit if the system command failed instead of blindly
continuing on.
In addition, only copy docs which exist, since now the copy failure will
cause the build to stop.
Closes#8455
Reported by the new script 'scripts/copyright.pl'. The script has a
regex whitelist for the files that don't need copyright headers.
Removed three (mostly usesless) README files from docs/
Closes#5141
