dud: A dub replacement

[Joseph Rushton Wakeling]

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. :-\