<div dir="ltr"><div dir="ltr"><br></div><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">On Wed, 18 Dec 2024 at 12:33, Zoltan Somogyi <<a href="mailto:zoltan.somogyi@runbox.com">zoltan.somogyi@runbox.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The diff makes and documents a choice; I would like<br>
people's opinions about that choice.<br></blockquote><div><br></div><div>> Install extra headers for PROPOSED installs.<br>> <br>> diff --git a/compiler/make.library_install.m b/compiler/make.library_install.m<br>> index 01f714df5..5b1e1d9c0 100644<br>> --- a/compiler/make.library_install.m<br>> +++ b/compiler/make.library_install.m<br><br>...<br><br>> +:- pred proposed_install_extra_headers(io.text_output_stream::in, globals::in,<br>> +    string::in,<br>> +    maybe_succeeded::in, maybe_succeeded::out, io::di, io::uo) is det.<br>> +<br>> +proposed_install_extra_headers(ProgressStream, Globals, Prefix,<br>> +        !Succeeded, !IO) :-<br>> +    globals.lookup_accumulating_option(Globals, extra_library_header,<br>> +        ExtraHdrFileNames),<br>> +    % We could install extra headers to a specialized directory,<br>> +    % or we could install them to the directory to which we install<br>> +    % either .mh or .mih files. Since .mih files are internal details<br>> +    % of the Mercury implementation, that choice looks wrong. The other two<br>> +    % are definitely defensible. The code below chooses the second alternative,<br>> +    % installing to the directory containing .mh files. The main advantage<br>> +    % of this choice is that it avoids the extra complication that an extra<br>> +    % directory to search for would mean for invoking the C compiler.<br><br>That was my reasoning back when I added the --extra-library-header option.<br><br>Julien.<br></div></div></div>