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