Ok
As I said to Bob, people could change how they use preferences


On 16/05/2018, 11:41, "Levente Uzonyi" <leves at caesar.elte.hu> wrote:

> Thankfully, we have the preference wizard, so we don't have to deal with 
the
> defaults any more. I would leave everything as-is.