am 05b0dcec: am 1eb2e84c: am 9da08122: More on issue #7318666: hide developer options from user build

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