Merge "More on issue #7318666: hide developer options from user build" into jb-mr1-dev