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!