am 9da08122: More on issue #7318666: hide developer options from user build

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