dud: A dub replacement

[Paolo Invernizzi]

On Monday, 18 November 2019 at 15:35:12 UTC, Joseph Rushton 
Wakeling wrote:
> On Monday, 18 November 2019 at 13:19:12 UTC, Paolo Invernizzi 
> wrote:
>> Closing this kind of discussions and letting anyone to choose 
>> "tabs or spaces" is a constructive solution, I think.
>
> It is quite extraordinary how readily folks fall to arguing 
> over what the config format should be, rather than what the app 
> should actually be able to do. :-\

Exactly, that's why I love pragmatism: let's dud emit the ones 
that are outdated, automatically.

Everyone can choose, work and update or the format he prefers, 
without impacting other people choices, and the discussion can 
move forward to something more interesting ...

my 2 cents, at least ...