[m-rev.] for post-commit review: install extra headers for PROPOSED

[Julien Fischer]

On Wed, 18 Dec 2024 at 12:33, Zoltan Somogyi <zoltan.somogyi at runbox.com>
wrote:

> The diff makes and documents a choice; I would like
> people's opinions about that choice.
>

> Install extra headers for PROPOSED installs.
>
> diff --git a/compiler/make.library_install.m
b/compiler/make.library_install.m
> index 01f714df5..5b1e1d9c0 100644
> --- a/compiler/make.library_install.m
> +++ b/compiler/make.library_install.m

...

> +:- pred proposed_install_extra_headers(io.text_output_stream::in,
globals::in,
> +    string::in,
> +    maybe_succeeded::in, maybe_succeeded::out, io::di, io::uo) is det.
> +
> +proposed_install_extra_headers(ProgressStream, Globals, Prefix,
> +        !Succeeded, !IO) :-
> +    globals.lookup_accumulating_option(Globals, extra_library_header,
> +        ExtraHdrFileNames),
> +    % We could install extra headers to a specialized directory,
> +    % or we could install them to the directory to which we install
> +    % either .mh or .mih files. Since .mih files are internal details
> +    % of the Mercury implementation, that choice looks wrong. The other
two
> +    % are definitely defensible. The code below chooses the second
alternative,
> +    % installing to the directory containing .mh files. The main
advantage
> +    % of this choice is that it avoids the extra complication that an
extra
> +    % directory to search for would mean for invoking the C compiler.

That was my reasoning back when I added the --extra-library-header option.

Julien.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20241219/c1d630dc/attachment.html>