On Mon, Sep 09, 2019 at 12:47:30PM +0200, Job Snijders wrote: > On Mon, Sep 09, 2019 at 10:22:53AM +0200, Otto Moerbeek wrote: > > So I tested that the setting below works: > > > > 1. New profile gets new default > > 2. Existing profile gets new default if user did not set it previously > > 3. Existing profile is not overriden if user set it previously. > > > > A user mailed me privately and confirmed this, > > > > So I think that is what we want, > > Elegant solution. I suspect you'll need to keep monitoring whether '5' > does today what it'll do tomorrow.
Yeah, do not trust upstream and verify ;-) > > > OK? > > OK job@ >
