dud: A dub replacement
paolo.invernizzi at gmail.com
Mon Nov 18 20:11:18 UTC 2019
On Monday, 18 November 2019 at 15:35:12 UTC, Joseph Rushton
> On Monday, 18 November 2019 at 13:19:12 UTC, Paolo Invernizzi
>> 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 ...
More information about the Digitalmars-d-announce