[m-rev.] for review: Add a tool to help maintain Copyright lines.

[Peter Wang]

On Fri, 09 Feb 2024 15:16:30 +1100 Peter Wang <novalazy at gmail.com> wrote:
> diff --git a/tools/update_copyright.pre-commit b/tools/update_copyright.pre-commit
> new file mode 100755
> index 000000000..af02913ee
> --- /dev/null
> +++ b/tools/update_copyright.pre-commit
> @@ -0,0 +1,32 @@
...
> +"$update_copyright" --suffix 'Mercury team' -- "${changed_files[@]}" &&
> +git add -u -- "${changed_files[@]}"

Actually, automatically running `git add` is not ideal as the user may
have some left some changes in the files that they did not want to
include in the commit. It's probably best to let the user add the
changed Copyright lines manually.

Peter