What to do if the option was set globally using the GlobalPreferences extension. ignore: Do nothing. The option remains with its previous value. override: Add a local override. update: Update the option globally.
