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
... when not actually following the redirect. Otherwise we return error
for this and an application can't extract the value.
Test 1518 added to verify.
Reported-by: Pavel Pavlov
Fixes#3340Closes#3364
