* commit 'fc31380adf4272c11bc32fab1dcea75804ad3166': More on issue #7318666: hide developer options from user build