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

[Zoltan Somogyi]

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 :-)

> That looks fine otherwise.

Thanks.

Zoltan.