On Tue, Sep 29, 2020 at 09:35:39AM +0200, Pavel Stehule wrote:
> +1
Thanks. I have applied this one. We may rework the handling of
redundant options for all commands to be more consistent in the
future, though it does not prevent fixing this issue until it
happens.
--
Michael