<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">On Mon, 15 Dec 2025 at 11:39, 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"><br>...<br>
<br>
Overall, the compiler pays attention to the value of the options_files option<br>
only when it decides in options_file.m what files to read. As you discovered,<br>
any changes after that have no effect. For the reasons above, I think that's fine.<br>
What is not fine is the absence of any mention of this limitation in the help text.<br>
I therefore propose that we add the following to that help text:<br>
<br>
Note that this option is intended to be used only on command lines.<br>
When specified in options files (i.e. in files named by --options-file options),<br>
it has no effect.<br></blockquote><div><br></div><div>That's fine.</div><div><br></div><div>Julien.</div></div></div>