[m-rev.] for review: Delete MERCURY_OPTIONS -r option (repeats).

[Zoltan Somogyi]

On 2023-07-13 04:55 +02:00 CEST, "Peter Wang" <novalazy at gmail.com> wrote:
> I always found the -r option questionable, but we can keep it if anyone
> still wants it.

The diff is fine.

> Other options that I think should be removed:
> 
>     -a  benchmark_all_solns
>     -t  use_own_timer (probably most useful with -r)

Agreed; remove them.

Zoltan.