On Tue, Jun 4, 2019 at 9:50 PM Thomas Stüfe <thomas.stu...@gmail.com> wrote:

>
> I would vote for keeping the name as it is: I would have to change a
> number of places, and when in doubt I'd like to keep the changes minimal to
> make backporting future changes easier.
>

OK - author gets to cast deciding vote!

Reply via email to