[m-rev.] for post-commit review: get tools/make_optimization_options to update compiler/options.m

[Julien Fischer]

On Fri, 18 Aug 2023, Zoltan Somogyi wrote:

>
> On 2023-08-18 13:21 +02:00 CEST, "Julien Fischer" <jfischer at opturion.com> wrote:
>>>> +/bin/rm .options_init .options_final handler_file > /dev/null 2>&1
>>
>> Any reason not to just use rm -f there?
>
> They both work. If I used -f, you could ask why I didn't redirect
> to /dev/null :-)

Let me reword that to: why did you not use the shorter from? ;-)

Julien.