[m-rev.] for review: Add copy_mercury_binaries script.

[Julien Fischer]

On Mon, 3 May 2021, Peter Wang wrote:

> tools/copy_mercury_binaries:
>    Add script to copy binaries from one Mercury installation
>    to another.
>
> README.cross:
>    Explain the use of the script.
>
>    Delete manual instructions.

That's fine

Julien.