[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#40863: [PATCH] Improve the display-time-world UI
From: |
Eli Zaretskii |
Subject: |
bug#40863: [PATCH] Improve the display-time-world UI |
Date: |
Mon, 27 Apr 2020 22:35:58 +0300 |
> From: Noam Postavsky <npostavs@gmail.com>
> Cc: 40863@debbugs.gnu.org, stefan@marxist.se
> Date: Mon, 27 Apr 2020 15:00:37 -0400
>
> No, I think changing the name here makes it more readable (i.e., it's
> not a random change, it's an improvement). And I think this benefit
> outweighs the possible existence of broken applications, or users
> possibly preferring the current value (I will admit this weighting also
> somewhat depends on the probability of these hypotheticals actually
> turning out to be real, which I've no real basis for; you might judge
> them to be more likely than I do).
I guess it's a matter of personal preferences, then. E.g., we have
*scratch* and *xref*.
bug#40863: [PATCH] Improve the display-time-world UI, Basil L. Contovounesios, 2020/04/27