[m-rev.] for review: delete Mercury.config.builtin.in

[Julien Fischer]

On Wed, 25 Jun 2025 at 03:29, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:

> Delete scripts/Mercury.config.bootstrap.in.
>
> scripts/Mercury.config.bootstrap.in:
>     Delete this file.
>
> configure.ac:
> scripts/Mmakefile:
>     Copy scripts/Mercury.config to scripts/Mercury.config.bootstrap.
>     Add a note about filtering out options that the installed compiler
>     does not yet understand.
>
> scripts/Mercury.config.in:
>     Document the new dual role of this file.
...
> diff --git a/scripts/Mmakefile b/scripts/Mmakefile
> index f95e3de27..7c9448f87 100644
> --- a/scripts/Mmakefile
> +++ b/scripts/Mmakefile


The clean_scripts target needs to be updated to remove
Mercury.config.bootstrap.

That looks ok otherwise.

Julien.