None of the other Options/Preferences pages have the word “Options”
in their names, because: a) it’s obvious that they’re options, and b)
having that word repeated there contravenes the macOS convention of
calling the options “preferences”.

Change-Id: I7349d20eefc50d5a92d6442a256249f64db688e7