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

[Zoltan Somogyi]

On Thu, 19 Dec 2024 00:41:48 +1100, Julien Fischer <jfischer at opturion.com> wrote:
> > +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.

Thanks for that. Could you please also take a look at the
diff that starts documenting the search options?

Zoltan.