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
This test verifies that the order of functions in public headers remain
the same but hasn't been updated to care for recently added header
files. The order is important for some few platforms - or VERSIONINFO
needs to updated.
This fix also updates VERSIONINFO to be sure.
Closes#8620
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